summaryrefslogtreecommitdiff
path: root/src/smt/abduction_solver.cpp
AgeCommit message (Expand)Author
2021-12-09Do not make SyGuS subsolver in unsat state after solving (#7759)Andrew Reynolds
2021-12-07Towards support for incremental sygus (#7736)Andrew Reynolds
2021-12-07Eliminate more static calls to Rewriter::rewrite (#7740)Andrew Reynolds
2021-10-09Remove static accesses to options where EnvObj is used (#7330)Gereon Kremer
2021-09-30Rename SmtEngine to SolverEngine. (#7282)Aina Niemetz
2021-09-30Rename files smt_engine.(cpp|h) to solver_engine.(cpp|h). (#7279)Aina Niemetz
2021-09-29Properly restrict PBE symmetry breaking for abduction queries (#7269)Andrew Reynolds
2021-09-03Eliminate backwards ref to SmtEngine from abduction and interpol solvers (#7133)Andrew Reynolds
2021-08-26Eliminate currentSmtEngine for subsolver calls (#7068)Andrew Reynolds
2021-05-27Fix spurious assertion for trivial abduction (#6629)Andrew Reynolds
2021-05-07Simplifications to expand definitions (#6487)Andrew Reynolds
2021-04-28Remove exception headers from options.h (#6456)Gereon Kremer
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
2020-10-12Eliminate uses of Expr in SmtEngine interface (#5240)Andrew Reynolds
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-08-18Split SygusSolver from SmtEngine (#4891)Andrew Reynolds
2020-07-15Use Nodes for SmtEngine assertions (#4752)Andres Noetzli
2020-07-15Split abduction solver from SmtEngine (#4733)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback