projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: eee1438) | patch
Split QuantElimSolver from SmtEngine (#4919)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 20 Aug 2020 11:04:43 +0000 (06:04 -0500)
committerGitHub <noreply@github.com>
Thu, 20 Aug 2020 11:04:43 +0000 (06:04 -0500)
commitc110363ccf39c9415c1a32bda6273fe8221db182
tree0d0ec2edc846b5c9a495ed29e077472ab74b0d40tree
parenteee14382af077bd043d53b75c038050b325dd04acommit | diff
Split QuantElimSolver from SmtEngine (#4919)

Towards refactoring SmtEngine / converting Expr -> Node.
src/CMakeLists.txt diff | blob | history
src/smt/command.cpp diff | blob | history
src/smt/quant_elim_solver.cpp [new file with mode: 0644] blob
src/smt/quant_elim_solver.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/quantifiers/sygus/synth_engine.cpp diff | blob | history