projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 77e9881) | patch
Split preprocessor from SmtEngine (#4854)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 6 Aug 2020 13:29:17 +0000 (08:29 -0500)
committerGitHub <noreply@github.com>
Thu, 6 Aug 2020 13:29:17 +0000 (08:29 -0500)
commit956ffda5632b388a887003a5e030696091339bd2
tree130b34e344ad9fa072d5c388132da0c5d0105c05tree
parent77e98815254c68301ffcd7fb8addeb6751c51187commit | diff
Split preprocessor from SmtEngine (#4854)

This splits a collection of utilities from SmtEngine that work in cooperation to preprocess assertions (Boolean circuit propagator, preprocessing context, process assertions, term formula removal).

It updates various interfaces in SmtEngine from Expr -> Node and simplifies SmtEngine to use this utility.
15 files changed:
src/CMakeLists.txt diff | blob | history
src/api/cvc4cpp.cpp diff | blob | history
src/printer/cvc/cvc_printer.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/smt/command.cpp diff | blob | history
src/smt/preprocessor.cpp [new file with mode: 0644] blob
src/smt/preprocessor.h [new file with mode: 0644] blob
src/smt/process_assertions.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/theory/quantifiers/candidate_rewrite_database.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
src/theory/theory_model.cpp diff | blob | history