Comments (2)
this is expected behavior: When you translate from one context to another, the new context inherits data-type declarations from the first.
from z3.
First, thanks for looking at it. It doesn't seem to be the behavior for all data types:
from z3 import *
def decl_A(ctx):
s = Datatype('A', ctx=ctx)
s.declare('b')
s.declare('c')
return s.create()
c = Context()
m = main_ctx()
decl_A(ctx=c)
x = Int('x', ctx=c)
x.translate(m)
decl_A(ctx=m)
does not throw any exception. I did not check if the data type A
is not translated back or just overwritten by the second declaration. Nevertheless, shouldn't the behavior be the same for all data types?
IMHO translating should only translate those data types the variable is dependent on, so I would expect the behavior of this example. But I might be wrong here.
To explain a bit further what I was doing: I was using context as namespaces. I have a function that solves a couple of SMT problems and declares data types to do that. It creates a context to keep these declarations local, translates in formulas from the main context, and translates the solutions (which don't use the data types) back to the main context. If that translation also translates back all the data types defined in that local context, I can basically not localize these declarations in a context because subsequent calls to that function will inherit the data type declarations from the main context to which they have been translated to by prior calls.
from z3.
Related Issues (20)
- Performance in multiple calls to solver HOT 1
- Assertion violation HOT 1
- Invalid model on float formula HOT 2
- [consolidated] hang on small instances (string, bit-vector) HOT 10
- DIMACS output bug
- TransitiveClosure + Quantifiers extremely slow HOT 1
- UNEXPECTED CODE WAS REACHED for recursive function HOT 2
- Dynamic library error HOT 1
- Bug in NLSAT,
- [feature request] output only necessary bindings HOT 1
- How to introduce Z3 in Visual Studio
- questions about the architecture of some release versions HOT 2
- Simplification yields f/n applied to x₁...xₘ with m≠n HOT 1
- RISC V build failures
- Z3 prover: this Smtlib shoud not be SAT because last assert, why? HOT 1
- [api bug?] Error("invalid argument") whenever no expr update
- ASSERT and python crashes HOT 3
- Performance regression on QF_NIA HOT 1
- Nested construction terms problem HOT 5
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from z3.