summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.h
AgeCommit message (Expand)Author
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
2018-01-24Commenting out throw specifiers on SmtEngine. These can later be refined into...Tim King
2018-01-03Global negate (#1466)Andrew Reynolds
2017-12-10Add new infrastructure for preprocessing passes (#1053)justinxu421
2017-12-06Add command for define-fun-rec and add to API (#1412)Andrew Reynolds
2017-11-15Adding garbage collection for Proof objects. (#1294)Tim King
2017-11-07Allow FORALL in quantifier elimination command (#1322)Andrew Reynolds
2017-10-11Move unsat core names to smt engine (#1192)Andrew Reynolds
2017-09-14Simplifying the throw specifier of SmtEngine::checkSat and related calls to C...Tim King
2017-07-19Removing the unused CDAttribute. This makes CDHashMap::obliterate unused. Rem...Tim King
2017-07-07Update copyright headers.Mathias Preiner
2017-05-12Make signal handlers saferAndres Notzli
2017-03-31Remove decl. of getStatisticsRegistry(SmtEngine*)Andres Notzli
2017-03-30[Coverity] Remove throw qualifiers in src/smtremove_throwAndres Notzli
2016-11-04Fix a few more minor memory leaks.ajreynol
2016-10-28Add get instantiations utilities to API.ajreynol
2016-04-20update from the masterPaulMeng
2016-01-28Adding listeners to Options.Tim King
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
2016-01-05Moving sexpr.{cpp,h,i} from expr/ back into util/.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback