summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.h
AgeCommit message (Expand)Author
2020-08-03Split expression names from SmtEngine (#4832)Andrew Reynolds
2020-08-03Split dump manager from SmtEngine (#4824)Andrew Reynolds
2020-07-31Split listener classes from SmtEngine (#4816)Andrew Reynolds
2020-07-28Replace Expr with Node in Term/Op (#4781)Andres Noetzli
2020-07-17Replace options listener infrastructure (#4764)Andrew Reynolds
2020-07-16Split abstract values utility from SmtEngine (#4754)Andrew Reynolds
2020-07-16Remove cumulative time limits and cpu time limits (#4711)Gereon Kremer
2020-07-15Use Nodes for SmtEngine assertions (#4752)Andres Noetzli
2020-07-15Split abduction solver from SmtEngine (#4733)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback