Stack Overflow
Stack Overflow

Questions tagged [cvc4]

CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.

75 questions
8
votes
2 answers

What are the limits of reasoning in quantified arithmetic in SMT?

I have tried several SMT solvers (CVC3, CVC4 and Z3) on the following seemingly trivial benchmark: (set-logic LIA) (set-info :smt-lib-version 2.0) (assert (forall (( x Int)) (forall ((y Int)) (= y x)))) (check-sat) (exit) The solvers all return…
Liana Hadarean
  • 81
  • 2
5
votes
2 answers

Exactly what quantifiers is SMT complete for?

I've been looking at various SMT solvers, mainly Z3, CVC4, and VeriT. They all have vague descriptions of their ability to solve SMT problems with quantifiers. Their documentation is primarily example based (Z3), or consists of academic papers,…
jmite
  • 8,171
  • 6
  • 40
  • 81
4
votes
1 answer

Does z3 support rational arithmetic for its input constraints?

In fact, does the SMT-LIB standard have a rational (not just real) sort? Going by its website, it does not. If x is a rational and we have a constraint x^2 = 2, then we should get back ``unsatisfiable''. The closest I could get to encoding that…
user1779685
  • 283
  • 2
  • 8
4
votes
2 answers

Dynamically call get-value only when check-sat returns "sat"

The SMT2 standard states that calling get-value is only legal after a call to check-sat and only when check-sat returns "sat" or "unknown". Here is a simple example of an unsat problem: (set-option :produce-models true) (set-logic QF_BV) (set-info…
Trevor Forentz
  • 147
  • 7
3
votes
1 answer

Get fractional part of real in QF_UFNRA

Using smtlib I would like to make something like modulo using QF_UFNRA. This disables me from using mod, to_int, to_real an such things. In the end I want to get the fractional part of z in the following code: (set-logic QF_UFNRA) (declare-fun z ()…
John Smith
  • 771
  • 8
  • 25
3
votes
1 answer

Meaning of (_ bv0 32), (_ bv1 16) ... in SMT2 benchmarks

I noticed that is some SMT2 benchmarks, notations like (_ bv0 32), (_ bv16 32), ... are used like, for instance,…
iguerNL
  • 464
  • 2
  • 8
2
votes
1 answer

Any comparison between different SMT solvers?

I have an implementation in Python that makes use of theorem proving. I would like to know if there is a possibility to speed up the SMT solving part, which is currently using Z3. I am trying to discover different solvers, and have found cvc4/cvc5…
Theo Deep
  • 666
  • 4
  • 15
2
votes
1 answer

How to declare forall quantifiers in SMTLIB / Z3 / CVC4?

I'm stuck on how to how to create a statement in SMTLIB2 that asserts something like forall x < 100, f(x) = 100 This property would be check a function that adds 1 to all numbers less than 100 recursively: (define-fun-rec incUntil100 ((x Int)) Int …
Alex Coleman
  • 607
  • 1
  • 4
  • 11
2
votes
1 answer

How to express set membership in SMTLIB format in Z3?

I'm trying to use the SMTLIB format to express set membership in Z3: (declare-const a (Set Int)) ;; the next two lines parse correctly in CVC4, but not Z3: (assert (= a (as emptyset (Set Int)))) (assert (member 12 a)) ;; these work in both…
Stefan Ciobaca
  • 138
  • 7
2
votes
1 answer

Type mismatch in smt2

The below smt2 code gives an error related to type. ( declare-datatypes ( ( List 1 ) ) ( ( par ( T ) ( ( cons ( hd T ) ( tl ( List T ) ) ) ( nil ) ) ) ) ) (declare-sort Ty 0) (define-fun-rec func ((x (List Ty) ) (y (List Ty))) (List…
Jagadeep Sai
  • 86
  • 8
2
votes
1 answer

difference in encoding of the same axiom

I'm wondering what is the difference between these two encoding of the same list axiom: (define-sort T1 () Int) (declare-fun list_length ( (List T1) ) Int) (assert (forall ( (i T1) (l (List T1)) ) (ite (= l (as nil (List T1))) …
JRR
  • 6,014
  • 6
  • 39
  • 59
2
votes
1 answer

define-fun vs define-funs-rec in smtlib

It seems that define-funs-rec is a strict superset of what define-fun can do according to the SMTLIB standard. If so is there a reason for not always using define-funs-rec, maybe except for syntactic simplicity?
JRR
  • 6,014
  • 6
  • 39
  • 59
2
votes
1 answer

Modelling a logic puzzle

I am trying to model a logic puzzle from To Mock a Mockingbird. I am struggling to translate it into SMT-LIB. The puzzle goes something like this: There is a garden in which all flowers are either red, yellow or blue, and all colours are…
buggymcbugfix
  • 321
  • 1
  • 11
2
votes
1 answer

CVC4 equivalent of Z3's seq.unit

I'm trying to run the following unsat example with both Z3 and CVC4. If I replace "\x00" with (seq.unit #x00) then it's not a problem for Z3, but CVC4 complains it doesn't know seq.unit. (declare-fun AB_serial_1_version_0 () String) (declare-fun…
OrenIshShalom
  • 5,974
  • 9
  • 37
  • 87
2
votes
1 answer

SMT Solver support for SMT-LIB 2.6 declare-datatypes statements

The draft for SMT-LIB Version 2.6 specifies a (declare-datatypes) statement. In the original announcement for this feature it is mentioned that the proposed syntax is different from the syntax supported by Z3 and CVC4 at the time. Is there any SMT…
CliffordVienna
  • 7,995
  • 1
  • 37
  • 57
1
2 3 4 5