summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.h
AgeCommit message (Expand)Author
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
2016-01-05Add SmtGlobals ClassTim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-10-26This commit fixes a bug related to a public header depending on a compiler fl...Tim King
2015-08-01Make --fmf-fun and --macros-quant work in incremental mode. Add regressions.ajreynol
2015-07-31Sygus support for inductive datatypes.ajreynol
2015-04-23Added option for --check-unsat-cores and various core bug fixes (merge of Mor...Liana Hadarean
2015-01-26Output solutions for synthesis conjectures with --dump-synth. Minor refactor...ajreynol
2014-11-17Resource-limiting work.Liana Hadarean
2014-10-23Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.Morgan Deters
2014-10-14Context-dependent expr attributes are now attached to a specific SmtEngine, a...Morgan Deters
2014-10-06Support for RESET command in CVC native language (and infrastructure for supp...Morgan Deters
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-08-18Add support for quantifier-specific instantiation levels. Add option for set...ajreynol
2014-07-01Update copyrights.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback