summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.h
AgeCommit message (Expand)Author
2020-07-11Towards Node-level SmtEnginenodeEmptySetAndres Noetzli
2020-07-07Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)Andrew Reynolds
2020-06-30Interpolation step 1 (#4638)Ying Sheng
2020-06-25Remove sygus1 parser (#4651)Andrew Reynolds
2020-06-18Add logic check for define-fun(s)-rec (#4577)Andres Noetzli
2020-06-16Update copyright headers.Aina Niemetz
2020-06-06Keep definitions when global-declarations enabled (#4572)Andres Noetzli
2020-06-04New C++ Api: Second and last batch of API guards. (#4563)Aina Niemetz
2020-04-08Split ProcessAssertions module from SmtEngine (#4210)Andrew Reynolds
2020-04-03Update theory rewriter ownership, add stats to strings (#4202)Andres Noetzli
2020-03-31Rename checkValid/query to checkEntailed. (#4191)Aina Niemetz
2020-03-31Remove replay and use-theory options and idl (#4186)Andrew Reynolds
2020-03-26Move set defaults function to its own file (#4154)Andrew Reynolds
2020-03-16SmtEngine: Convert members owned by SmtEngine to unique pointers. (#4108)Aina Niemetz
2020-03-10Fix issue with reset-assertions. (#3988)Aina Niemetz
2020-03-05Move ownership of DecisionEngine into PropEngine. (#3850)Aina Niemetz
2020-03-05Revert "Move ownership of DecisionEngine into PropEngine. (#3850)"Aina Niemetz
2020-03-05Move ownership of DecisionEngine into PropEngine. (#3850)Andrew Reynolds
2020-02-26Remove portfolio leftovers (#3821)Andres Noetzli
2019-11-13Distinguish unknown status for model printing (#3454)Andrew Reynolds
2019-11-04Make getSynthSolution return a Bool (#3306)Andrew Reynolds
2019-09-04Towards incremental SyGuS in SMT engine (#3195)Andrew Reynolds
2019-08-19New C++ API: Add checks for Solver::checkValid and Solver::checkValidAssuming...Aina Niemetz
2019-08-14Call separate SMT engine for single invocation sygus (#3151)Andrew Reynolds
2019-08-13SmtEngine: Reorganize class according to guidelines, some cleanup. (#3183)Aina Niemetz
2019-08-13 Track sygus variable to term relationship via attribute (#3182)Andrew Reynolds
2019-08-13Implement check abduct feature (#3152)Andrew Reynolds
2019-08-07New C++ API: Add checks and tests for push/pop. (#3121)Aina Niemetz
2019-08-02Flip the polarity of the argument of get-abduct (#3153)Andrew Reynolds
2019-07-30 Track solver execution mode (#3132)Andrew Reynolds
2019-07-29Model blocker feature (#3112)Andrew Reynolds
2019-07-29Support get-abduct smt2 command (#3122)Andrew Reynolds
2019-06-04Add check that result matches benchmark status (#3028)Andres Noetzli
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
2019-03-26Update copyright headers.Aina Niemetz
2019-03-19Sygus abduction feature (#2744)Andrew Reynolds
2019-01-11New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)Aina Niemetz
2018-10-18Introducing internal commands for SyGuS commands (#2627)Haniel Barbosa
2018-08-23Makes the filename be set in the SMT engine by default (#2366)Haniel Barbosa
2018-08-15Fix dumping of get-unsat-assumptions (#2302)Andres Noetzli
2018-08-07Delete functions instead of using CVC4_UNDEFINED (#1794)Andres Noetzli
2018-07-31Improvements and tests for the API around separation logic (#2229)ayveejay
2018-07-24Adding API access methods to get heap/nil expressions when using separation l...ayveejay
2018-05-22Make sygus infer find function definitions (#1951)Andrew Reynolds
2018-03-13SmtEngine::getModel() is now public. (#1665)Aina Niemetz
2018-03-09Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)Aina Niemetz
2018-03-05Add support for check-sat-assuming. (#1637)Aina Niemetz
2018-03-02Fixed comments in smt_engine.h.Aina Niemetz
2018-02-28SmtEngine::getAssignment now returns a vector of assignments. (#1628)Aina Niemetz
2018-02-02Option to check solutions produced by SyGuS solver (#1553)Haniel Barbosa
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback