projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e63abd2) | patch
Model generation for arith, boolean, and uf theories via
authorMorgan Deters <mdeters@gmail.com>
Sat, 9 Oct 2010 04:24:15 +0000 (04:24 +0000)
committerMorgan Deters <mdeters@gmail.com>
Sat, 9 Oct 2010 04:24:15 +0000 (04:24 +0000)
commit97668b64994c5749a5a75822136de49841d2c15d
tree23dd1852741a847f6228cc063b0a5ad7ec3c2af3tree
parente63abd23b45a078a42cafb277a4817abb4d044a1commit | diff
Model generation for arith, boolean, and uf theories via
(get-value ...) SMT-LIBv2 command.  As per SMT-LIBv2 spec,
you must pass --interactive --produce-models on the command
line (although they don't currently make us do any extra
work).  Closes bug #213.
31 files changed:
src/expr/node_value.cpp diff | blob | history
src/expr/type.h diff | blob | history
src/parser/smt2/Smt2.g diff | blob | history
src/prop/cnf_stream.h diff | blob | history
src/prop/prop_engine.cpp diff | blob | history
src/prop/prop_engine.h diff | blob | history
src/prop/sat.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/theory/arith/delta_rational.cpp diff | blob | history
src/theory/arith/delta_rational.h diff | blob | history
src/theory/arith/tableau.cpp diff | blob | history
src/theory/arith/tableau.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.cpp diff | blob | history
src/theory/booleans/theory_bool.h diff | blob | history
src/theory/builtin/theory_builtin.cpp diff | blob | history
src/theory/builtin/theory_builtin.h diff | blob | history
src/theory/bv/theory_bv.cpp diff | blob | history
src/theory/bv/theory_bv.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/morgan/theory_uf_morgan.cpp diff | blob | history
src/theory/uf/morgan/theory_uf_morgan.h diff | blob | history
src/theory/uf/tim/theory_uf_tim.h diff | blob | history
src/util/congruence_closure.h diff | blob | history
src/util/result.h diff | blob | history