Questions tagged [smt-lib]
27 questions
2
votes
1 answer
Are Int and Real somehow compatible in SMT-LIB?
The equality operator in SMT-LIB generally requires, unsurprisingly, that its operands be of the same type. For example, this is an error:
(set-logic QF_LIRA)
(declare-fun a () Bool)
(declare-fun b () Real)
(assert (= a b))
(check-sat)
However, I…
rwallace
- 31,405
- 40
- 123
- 242
1
vote
1 answer
Is there a compliant way to let z3 recognize a term with a polymorphic datatype's tester well sorted in general?
As pointed out in this issue, Z3 cannot handle the following code correctly, meaning that Z3 reports the error (error "line 6 column 15: ambiguous function declaration reference, provide full signature to disambiguate ( (*) )…
Yuki
- 13
- 3
1
vote
1 answer
What is on earth difference between QF_LRA and QF_NRA in Z3
Theoretically, these 2 logics have some difference in Z3. But when I try to code, it seems that there is no difference between them.
For example, the code below should have showed the difference:
from z3 import *
# create variables
x = Real('x')
y…
Jrzhao
- 13
- 2
1
vote
1 answer
Why does smtlib/z3/cvc4 allow to declare the same constant more than once?
I have a question about declare-const in smtlib.
For example,
In z3/cvc4, the following program doesn't report an error:
C:\Users\Chansey>z3 -in
(declare-const x Int)
(declare-const x Bool)
In the smt-lib-reference, it says that
(declare-fun f (s1…
chansey
- 1,266
- 9
- 20
1
vote
1 answer
Is it possible to encode conditional sat checks in Z3?
Suppose I have the following problem (which I've made trivial to simplify my question)
;; declare variables
(declare-const X0 Int)
(assert (>= X0 0))
(assert (<= X0 1))
(declare-const X1 Int)
(assert (>= X1 0))
(assert (<= X1 1))
(declare-const X2…
HXSP1947
- 1,311
- 1
- 16
- 39
1
vote
1 answer
Regex to interpret smtlib2 format
I am trying to figure out a regex that could match results of a program that outputs in the smtlib format. Basically, my data is in the form:
(define-fun X_1 () Int
281)
(define-fun X_71 () Int
104)
(define-fun X_90 () Int
21)
…
Stefan Kovacs
- 65
- 5
1
vote
1 answer
Is there an operator for inequality in SMT-Lib?
I know I can assert inequality with simple (not (= a b)), but I wonder if there is a operator that does this directly. I have tried everything that came to my mind including !=, <>, \= (this doesn't parse), /=, =/=, neq and none of them works.
Is…
radrow
- 6,419
- 4
- 26
- 53
0
votes
0 answers
Python smtplib EmailMessage make_msgid renders elements and images incorrectly / wrong
I developing email-delivery (email-sending) for a company. This project is being developed for debt collection.
For project i use next stack and libraries:
python
smtlib
email
I designed html-template for email-message:
imartov
- 17
- 4
0
votes
1 answer
Does there exist an SMT library with a theory for sets?
Here are some examples of how what I'm describing would work:
(define-set Complex)
(define-set Imaginary)
(define-set Real)
(define-set Integers)
(define-set Positive)
; define properties these sets must follow
(assert (subset Imaginary…
Tilo RC
- 11
- 2
0
votes
1 answer
Can the type of a variable in Z3 be dynamically redefined in a formula?
For example, consider the formula from SymPy's new assumptions:
(x>2) & (y>0) & (Q.integer(y) | (y>10))
The expressions (Q.integer(y) | (y>10)) means that y is an integer or y is greater than 10 (or both). If it's not an integer then it would be a…
Tilo RC
- 11
- 2
0
votes
1 answer
How can I convert an SMT model with optimization using z3 library to a .smt2 file recognized by different solvers like cvc4?
I want to convert an SMT model written in python using z3 library in a file .smt2 to obtain a file which can be run from different solvers (for instance cvc4-solver).
The problem is that my model makes optimization and when there is a conversion…
0
votes
1 answer
What is the function associated with seq.map in C API of z3?
I want to know is their function in z3.h that is related to seq.map in SMT-LIB2 that explained below
text
thanks for any help
i searched and saw z3.h but cant find any function
0
votes
1 answer
How do I make z3 float solution not random
I am currently doing regression testing so I need the fixed results rather than random ones. I have tried all the methods including setting the random seed to 0, set_option('smt.arith.random_initial_value',False) and others. But nothing changes. The…
Jrzhao
- 13
- 2
0
votes
1 answer
Finding real solutions to problem is slower than expected
Sorry this is a basic question, I'm new to z3.
I wrote a program to find a real solution to a certain equation. Since it should be generated for every equation, I can't simplify the equation to much beforehand. But the program is really slow. It is…
Jerôme
- 3
- 1
0
votes
1 answer
Theory of arrays in Z3: (1) model is difficult to understand, (2) do not know how to implement functions and (3) difference with sequences
Following to the question published in How expressive can we be with arrays in Z3(Py)? An example, I expressed the following formula in Z3Py:
Exists i::Integer s.t. (0<=i<|arr|) & (avg(arr)+t
Theo Deep
- 666
- 4
- 15