summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
2017-11-14Make QEffort an enum (#1366)Andrew Reynolds
2017-11-14(Refactor) Split sygus term db (#1335)Andrew Reynolds
2017-11-14Clean Ceg Instantiators (#1365)Andrew Reynolds
2017-11-14Initializes InstPropagator::d_has_relevant_inst. Resolves 1362891. (#1360)Tim King
2017-11-13(Refactor) Decouple rep set iterator and quantifiers (#1339)Andrew Reynolds
2017-11-13Argument Relevance for Synthesis Conjectures (#1311)Andrew Reynolds
2017-11-13Initializes CegConjectureSingleInvSol::d_root_id. (#1361)Tim King
2017-11-09Higher-order prep (#1338)Andrew Reynolds
2017-11-09 Decouple sygus term database and term database. (#1317)Andrew Reynolds
2017-11-07Initializing QModelBuilder members. (#1334)Tim King
2017-11-07Guard relevant domain computation properly, minor. (#1325)Andrew Reynolds
2017-11-07Initializing NegContainsSygusInvarianceTest::d_cpbe in constructor. (#1328)Tim King
2017-11-06Using unique_ptr's for members of CegConjecture. (#1324)Tim King
2017-11-06Updates to interface for Sygus grammar construction. (#1323)Andrew Reynolds
2017-11-06Unrecurisify rewrite solve assertion for cbqi bv (#1312)Andrew Reynolds
2017-11-01(Move-only) Split quant util (#1306)Andrew Reynolds
2017-11-01(Refactor) Split term util (#1303)Andrew Reynolds
2017-11-01CBQI BV choice expressions (#1296)Andrew Reynolds
2017-11-01(Move-only) Refactor and document theory model part 2 (#1305)Andrew Reynolds
2017-10-31CID 1459592: Always checking whether rd is null or not. (#1299)Tim King
2017-10-28(Move only) Move enumerative instantiation strategy to its own file and docum...Andrew Reynolds
2017-10-28Sygus process conjecture (#1286)Andrew Reynolds
2017-10-28Document term db (#1220)Andrew Reynolds
2017-10-27Document quant arith (#1271)Andrew Reynolds
2017-10-27Cbqi multiple instantiation (#1289)Andrew Reynolds
2017-10-27Refactor theory model (#1236)Andrew Reynolds
2017-10-25CBQI BV: Add handling for missing operators. (#1274)Aina Niemetz
2017-10-24Cbqi bv ineq mode (#1273)Andrew Reynolds
2017-10-24Removing deprecated file. (#1270)Andrew Reynolds
2017-10-23CBQI BV: Add ULT/SLT inverse handling. (#1268)Aina Niemetz
2017-10-23Document sygus programming-by-examples utility (#1260)Andrew Reynolds
2017-10-20Make Sygus conjectures higher-order (#1244)Andrew Reynolds
2017-10-19CBQI BV: Refactor solve_bv_constraint. (#1265)Aina Niemetz
2017-10-16Sygus enumerators to conjecture (#1237)Andrew Reynolds
2017-10-13CBQI BV: Added EXTRACT handling. (#1240)Aina Niemetz
2017-10-12CBQI BV quick heuristics (#1239)Andrew Reynolds
2017-10-12Initial support for solving bit-vector inequalities (#1229)Andrew Reynolds
2017-10-11Enable regressions for CBQI BV and fix inverse for LSHR. (#1234)Aina Niemetz
2017-10-11Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224)Mathias Preiner
2017-10-11Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion ...Andrew Reynolds
2017-10-09Split term database (#1206)Andrew Reynolds
2017-10-09CBQI BV: Add inverse for more operators. (#1213)Aina Niemetz
2017-10-05Ho model (#1120)Andrew Reynolds
2017-10-04Ho quant util (#1119)Andrew Reynolds
2017-10-03Move sygus grammar utilities to separate file. (#1184)Andrew Reynolds
2017-10-02Address comments from PR #1164. (#1174)Mathias Preiner
2017-10-01CID 1457268: Initializing CegConjecture::d_syntax_guided to false. (#1181)Tim King
2017-09-30SyGuS streaming solution mode (#1131)Andrew Reynolds
2017-09-29Move BvInverter class into separate file. (#1173)Mathias Preiner
2017-09-29Simplify representation of inversion Skolems for bv cegqi (#1164)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback