projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: adae14a) | patch
changing theoryOf in shared mode with arrays to move equalities to arrays
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Sat, 16 Jun 2012 21:35:05 +0000 (21:35 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Sat, 16 Jun 2012 21:35:05 +0000 (21:35 +0000)
commitbc36750b551f1d0b571af1e2265b5dea42544e7d
tree4d8621cce48900fe3220d55b5fb451adeb125607tree
parentadae14a07b1019d092b4d5aa0cf809f9d0eca66dcommit | diff
changing theoryOf in shared mode with arrays to move equalities to arrays
disabled in bitvectors due to non-stably infinite problems

the option to enable it is --theoryof-mode=term
14 files changed:
src/smt/smt_engine.cpp diff | blob | history
src/theory/Makefile.am diff | blob | history
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/rewriter.cpp diff | blob | history
src/theory/theory.cpp diff | blob | history
src/theory/theory.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theoryof_mode.h [new file with mode: 0644] blob
src/theory/uf/theory_uf.cpp diff | blob | history
src/util/options.cpp diff | blob | history
src/util/options.h diff | blob | history
test/regress/regress0/aufbv/Makefile.am diff | blob | history
test/regress/regress0/aufbv/fifo32bc06k08.delta01.smt [new file with mode: 0644] blob
test/regress/regress0/unconstrained/Makefile.am diff | blob | history