projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7adcbaf) | patch
Some base infrastructure for user push/pop; a few bugfixes to user push/pop and model...
authorMorgan Deters <mdeters@gmail.com>
Thu, 29 Sep 2011 05:15:30 +0000 (05:15 +0000)
committerMorgan Deters <mdeters@gmail.com>
Thu, 29 Sep 2011 05:15:30 +0000 (05:15 +0000)
commitc94347913fa464b1ec6a3da2ab21e319c0c42e02
tree6c8252385365e5dacc86ce8c364c3d06332d39a7tree
parent7adcbaf2eac82be6ca8cf1569bab80c961710950commit | diff
Some base infrastructure for user push/pop; a few bugfixes to user push/pop and model gen also.
I also expect this commit to fix bug #273.

No performance change is expected on regressions with this commit, see
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
31 files changed:
Makefile.am diff | blob | history
Makefile.builds.in diff | blob | history
src/context/cdmap.h diff | blob | history
src/context/context.h diff | blob | history
src/expr/expr_manager_template.cpp diff | blob | history
src/main/interactive_shell.cpp diff | blob | history
src/main/interactive_shell.h diff | blob | history
src/prop/minisat/core/Solver.cc diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/theory/arith/theory_arith.cpp diff | blob | history
src/theory/arith/theory_arith.h diff | blob | history
src/theory/arrays/theory_arrays.cpp diff | blob | history
src/theory/arrays/theory_arrays.h diff | blob | history
src/theory/booleans/theory_bool.h diff | blob | history
src/theory/builtin/theory_builtin.h diff | blob | history
src/theory/bv/theory_bv.h diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.h diff | blob | history
src/theory/example/theory_uf_tim.cpp diff | blob | history
src/theory/example/theory_uf_tim.h diff | blob | history
src/theory/substitutions.cpp diff | blob | history
src/theory/substitutions.h diff | blob | history
src/theory/theory.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history
src/theory/uf/theory_uf.h diff | blob | history
test/unit/prop/cnf_stream_black.h diff | blob | history
test/unit/theory/theory_arith_white.h diff | blob | history
test/unit/theory/theory_black.h diff | blob | history
test/unit/theory/theory_engine_white.h diff | blob | history