summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
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
2018-11-21Quickly recognize when PBE conjectures are infeasible (#2718)Andrew Reynolds
2018-11-15 Expand definitions prior to model core computation (#2707)Andrew Reynolds
2018-10-31Record assumption info in AssertionPipeline (#2678)Andres Noetzli
2018-10-22Recover from wrong use of get-info :reason-unknown (#2667)Andres Noetzli
2018-10-19Sygus streaming non-implied predicates (#2660)Andrew Reynolds
2018-10-18Add OptionException handling during initialization (#2466)Andres Noetzli
2018-10-18Non-implied mode for model cores (#2653)Andrew Reynolds
2018-10-18Introducing internal commands for SyGuS commands (#2627)Haniel Barbosa
2018-10-17Sygus query generator (#2465)Andrew Reynolds
2018-10-15Delay initialization of theory engine (#2621)Andrew Reynolds
2018-10-12Reset input language for ExprMiner subsolver (#2624)Andres Noetzli
2018-10-10Fix default setting of CegisUnif options (#2605)Haniel Barbosa
2018-10-10Synthesize rewrite rules from inputs (#2608)Andrew Reynolds
2018-10-08Fix compiler warnings. (#2601)Aina Niemetz
2018-10-05Update default options for sygus (#2586)Andrew Reynolds
2018-10-01 Fix dumping pre/post preprocessing passes (#2469)Andres Noetzli
2018-10-01Refactor preprocessing pass registration (#2468)Andres Noetzli
2018-09-22cmake: Remove unused CMakeLists.txtMathias Preiner
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-09-18Move and rename sygus solver classes (#2488)Andrew Reynolds
2018-09-18fix assertion error (#2487)Haniel Barbosa
2018-09-17Remove broken dumping support from portfolio build (#2470)Andres Noetzli
2018-09-17Remove unnecessary tracing from preprocessing (#2472)Andres Noetzli
2018-09-14Refactor how assertions are added to decision engine (#2396)Andres Noetzli
2018-09-11Support model cores via option --produce-model-cores. (#2407)Andrew Reynolds
2018-09-10Refactor non-clausal simplify preprocessing pass. (#2425)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback