summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2019-09-16Return RecoverableModalException when model is not available. (#3283)Andrew Reynolds
2019-09-12Encapsulate synth engine (#3271)Andrew Reynolds
2019-09-06Remove portfolio (#3236)Andrew Reynolds
2019-09-05 Model API for domain elements (#3243)Andrew Reynolds
2019-09-04Towards incremental SyGuS in SMT engine (#3195)Andrew Reynolds
2019-08-28Removing comments related to issues (#3232)Andrew Reynolds
2019-08-27Fixes for get-abduct (#3229)Andrew Reynolds
2019-08-19New C++ API: Add checks for Solver::checkValid and Solver::checkValidAssuming...Aina Niemetz
2019-08-14Remove option --continued-execution. (#3189)Mathias Preiner
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-05Remove forward declarations in quantifiers engine (#3156)Andrew Reynolds
2019-08-02Flip the polarity of the argument of get-abduct (#3153)Andrew Reynolds
2019-08-01Enable sygus logic when produce-abducts is true (#3144)Andrew Reynolds
2019-08-01 Regular expression intersection modes (#3134)Andrew Reynolds
2019-07-30 Track solver execution mode (#3132)Andrew Reynolds
2019-07-30Code to activate hoelim preprocessing pass (#3129)Haniel Barbosa
2019-07-29Model blocker feature (#3112)Andrew Reynolds
2019-07-29Support get-abduct smt2 command (#3122)Andrew Reynolds
2019-07-01Support sygus version 2 format (#3066)Andrew Reynolds
2019-06-21Fix and simplify handling of --force-logic (#3062)Andres Noetzli
2019-06-11Disable dumping regression for non-dumping builds (#3046)Andres Noetzli
2019-06-11 Fix spurious assertion in get-value (#3052)Andrew Reynolds
2019-06-05Add support for SWIG 4 (#3041)Andres Noetzli
2019-06-04Enable proof checking for QF_LRA benchmarks (#2928)Andres Noetzli
2019-06-04Add check that result matches benchmark status (#3028)Andres Noetzli
2019-05-15Fix iterators in Java API (#3000)Andres Noetzli
2019-04-29Eliminate APPLY kind (#2976)Andrew Reynolds
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
2019-04-17More use of isClosure (#2959)Andrew Reynolds
2019-04-11 Eliminate Boolean ITE within terms, fixes 2947 (#2949)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2019-03-22Use empty vector instead of false in query with null Expr assumption (#2876)makaimann
2019-03-19Sygus abduction feature (#2744)Andrew Reynolds
2019-03-16Limit --solve-int-as-bv=X to QF_NIA/QF_LIA/QF_IDL (#2868)Andres Noetzli
2019-03-14check for null assumption in query and replace with false (#2858)makaimann
2019-03-13Add statistics for proof gen./checking time, size (#2850)Andres Noetzli
2019-02-27Use string stream for proofs instead of tmp files (#2841)Andres Noetzli
2019-02-12Delete temporary proof files when aborting CVC4 (#2834)Andres Noetzli
2019-01-18 Fix ABC build (#2808)Andres Noetzli
2019-01-15Strings: Add option to change loop process mode (#2794)Andres Noetzli
2019-01-11New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)Aina Niemetz
2018-12-11Remove alternate versions of mbqi (#2742)Andrew Reynolds
2018-12-10BoolToBV modes (off, ite, all) (#2530)makaimann
2018-12-06Fix use-after-free due to destruction order (#2739)Andres Noetzli
2018-11-29Combine sygus stream with PBE (#2726)Andrew Reynolds
2018-11-27Lazy model construction in TheoryEngine (#2633)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback