projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c460fd4) | patch
Split SygusSolver from SmtEngine (#4891)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 18 Aug 2020 16:41:46 +0000 (11:41 -0500)
committerGitHub <noreply@github.com>
Tue, 18 Aug 2020 16:41:46 +0000 (11:41 -0500)
commitab9742939d7706e10ea3d70c73275e97a5235f03
treed7d08da62cc172bdd8940357c27d848dc9e3c04ctree
parentc460fd4ba1cdacf04305475e605071889ed0e92fcommit | diff
Split SygusSolver from SmtEngine (#4891)

This is the solver for standard SyGuS queries. Notice it now depends only on SmtSolver and not SmtEngine.

This PR updates Expr -> Node for the sygus interface in SmtEngine.

SmtEnginePrivate is no longer needed and is deleted with this PR.
src/CMakeLists.txt diff | blob | history
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/command.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/smt/sygus_solver.cpp [new file with mode: 0644] blob
src/smt/sygus_solver.h [new file with mode: 0644] blob
src/theory/quantifiers/sygus/sygus_interpol.cpp diff | blob | history