projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f1351ca) | patch
Use Nodes for SmtEngine assertions (#4752)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 15 Jul 2020 23:42:00 +0000 (16:42 -0700)
committerGitHub <noreply@github.com>
Wed, 15 Jul 2020 23:42:00 +0000 (18:42 -0500)
commit3b87ce3ab67fd463a733ad11402e32f94eb1017e
treef58e422e35ca61ca61045f09643d61d2e500a77ctree
parentf1351ca7462d3d601e0dec78b71f54e0c7ee381fcommit | diff
Use Nodes for SmtEngine assertions (#4752)

This commit changes SmtEngine::assertFormula() to use Nodes rather
than Exprs and changes AssertionList to be Node-based. This is
work towards removing the Expr layer.
src/api/cvc4cpp.cpp diff | blob | history
src/preprocessing/passes/sygus_inference.cpp diff | blob | history
src/smt/abduction_solver.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/theory/quantifiers/expr_miner.cpp diff | blob | history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp diff | blob | history
src/theory/quantifiers/sygus/cegis_core_connective.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_repair_const.cpp diff | blob | history
src/theory/smt_engine_subsolver.cpp diff | blob | history
test/system/CMakeLists.txt diff | blob | history