summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
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
2017-09-29Initial working version of BV word-level instantiation (#1158)Andrew Reynolds
2017-09-28Cegqi refactor prep bv (#1155)Andrew Reynolds
2017-09-28Improve finite model finding for recursive predicates (#1150)Andrew Reynolds
2017-09-27Minor fixes for partial quantifier elimination. (#1147)Andrew Reynolds
2017-09-27CEGQI for BV: Add inverse for BITVECTOR_MULT. (#1153)Aina Niemetz
2017-09-25Cegqi refactor substitutions (#1129)Andrew Reynolds
2017-09-25Fixing CID 1362917: There was a branch where d_issup was not initialized. Swi...Tim King
2017-09-21Sygus inv templ refactor (#1110)Andrew Reynolds
2017-09-19Refactor cegqi instantiation infrastructure so that it is more independent of...Andrew Reynolds
2017-09-12Initial infrastructure for BV instantiation via word-level inversions. (#1056)Andrew Reynolds
2017-08-17Add mbqi interleave option, change option fs-inst to fs-interleave.ajreynol
2017-08-14Move function defns from smt_engine_scope.h to cpp (#216)Andres Noetzli
2017-08-07Fix compiler warning in theory/quantifiers/term_database_sygus.cppAina Niemetz
2017-08-07Change sygus output for failed reconstruction case.ajreynol
2017-07-31Minor improvement for enumerative instantiation.ajreynol
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
2017-07-20Fix a few bugs related to sygus.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback