projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 468c5bc) | patch
Added preprocessing pass that propagates unconstrained values - solves all of
authorClark Barrett <barrett@cs.nyu.edu>
Mon, 4 Jun 2012 22:26:40 +0000 (22:26 +0000)
committerClark Barrett <barrett@cs.nyu.edu>
Mon, 4 Jun 2012 22:26:40 +0000 (22:26 +0000)
commit3609fb41d7744b3a7d74e44f7bedc4d4c522c938
tree011a3fa796fdb98bb3b9a1b425d12c678535f294tree
parent468c5bc5d8b63ec6818813270225e09383dd79ffcommit | diff
Added preprocessing pass that propagates unconstrained values - solves all of
the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help
generally on at least BV and maybe others.
Off by default for now - results are mixed and it's hard to evaluate with so
many existing assertion failures and segfaults - will re-evaluate once those
are fixed
67 files changed:
src/expr/node.h diff | blob | history
src/parser/smt/smt.cpp diff | blob | history
src/parser/smt/smt.h diff | blob | history
src/parser/smt2/smt2.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/theory/Makefile.am diff | blob | history
src/theory/booleans/circuit_propagator.h diff | blob | history
src/theory/bv/theory_bv_rewrite_rules_normalization.h diff | blob | history
src/theory/substitutions.cpp diff | blob | history
src/theory/substitutions.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history
src/util/options.cpp diff | blob | history
src/util/options.h diff | blob | history
test/regress/regress0/unconstrained/Makefile.am [new file with mode: 0644] blob
test/regress/regress0/unconstrained/arith.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/arith2.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/arith3.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/arith4.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/arith5.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/arith6.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/arith7.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/array1.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvbool.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvbool2.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvbool3.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvbool3.smt3 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvcmp.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvconcat.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvconcat2.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvdiv.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvdiv2.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvext.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvite.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvmul.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvmul2.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvmul3.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvnot.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvsle.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvsle2.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvsle3.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvsle4.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvsle5.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvslt.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvslt2.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvslt3.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvslt4.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvslt5.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvule.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvule2.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvule3.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvule4.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvule5.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvult.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvult2.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvult3.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvult4.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/bvult5.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/files [new file with mode: 0644] blob
test/regress/regress0/unconstrained/geq.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/gt.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/leq.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/lt.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/uf1.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/uf2.smt2 [new file with mode: 0644] blob
test/regress/regress0/unconstrained/xor.smt2 [new file with mode: 0644] blob