z3

115 Questions
Newest Active Unanswered Frequent
Score
View
Card Compact
When will the SMT-LIB standard be extended to include optimization?
user_102643220
•
1
1
42
smt z3
z3 returning unknown when using Floats and Reals together?
user_146934600
•
1
1
42
smt z3
How to use soft constraints in Z3-Python to express 'abstract' biases in SAT search: such as 'I prefer half of the literals to be true and half false'
user_140823850
•
1
1
166
satisfiability theorem-proving z3py z3 sat
Algebraic numbers in Z3
user_108024730
•
1
1
79
z3py z3
References for Z3 - how does it work[internal theory]?
user_65775030
•
2
1
129
z3
How to bias Z3's (Python) SAT solving towards a criteria, such as 'preferring' to have more negated literals
user_140823850
•
2
2
110
satisfiability theorem-proving z3py z3 sat
Use Z3 to find counterexamples for a 'guess solution' to a particular CHC system?
user_65775030
•
1
1
64
z3py z3
Z3 Python: ordering models and accessing their elements
user_140823850
•
2
1
110
z3py z3 variable-assignment list python
Add binary operator to z3
user_171013300
•
3
1
115
z3 parsing python
Can the mkOr(Expr<BoolSort> ... t) fuction in the Z3 Java Api get a list as input?
user_86271800
•
2
1
49
smt z3 solver java
Hot Questions