projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ea22ebc) | patch
Refactor the theory specific parts of definition expansion into the theory solvers.
authorMartin Brain <>
Tue, 11 Mar 2014 00:03:41 +0000 (00:03 +0000)
committerMorgan Deters <mdeters@cs.nyu.edu>
Wed, 19 Mar 2014 20:55:22 +0000 (16:55 -0400)
commit9d855960ba88c9b476ab1be17b7686c009f516f5
tree143f12b95eb7563b3186658c20c8fa45236b2aa4tree
parentea22ebcbd69b24906d2214b7d294261578ce67a7commit | diff
Refactor the theory specific parts of definition expansion into the theory solvers.

In the process of doing this I may have fixed some bugs or some potential bugs so there
may be some user visible results of this refactoring.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
13 files changed:
src/Makefile.am diff | blob | history
src/smt/logic_request.h [new file with mode: 0644] blob
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/arith/theory_arith_private.cpp diff | blob | history
src/theory/arith/theory_arith_private.h diff | blob | history
src/theory/bv/theory_bv.cpp diff | blob | history
src/theory/bv/theory_bv.h diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings.h diff | blob | history
src/theory/theory.h diff | blob | history