summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2017-10-27Improve strings rewriter for contains (#1207)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-27Implement Hilbert choice operator (#1291)Andrew Reynolds
2017-10-25Removing throw specifiers from OutputChannel and subclasses. (#1209)Tim King
2017-10-25Switching EqProof to use shared_ptr everywhere. (#1217)Tim King
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-20Add rewriting rules for Eq/Ult with sign_extend and constants. (#1258)Mathias Preiner
2017-10-20Simplify atoms introduced while bitblasting. (#1267)Mathias Preiner
2017-10-20SyGuS term size limit (#1262)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-17Fixing 2 instances of an unused variable. (#1253)Tim King
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-11Cleaning up ProofArray class. (#1208)Tim King
2017-10-11Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion ...Andrew Reynolds
2017-10-10Ho node manager types (#1203)Andrew Reynolds
2017-10-10Fix memory leak in quantifiers engine (#1219)Andres Noetzli
2017-10-09Add skeleton of the FP theory solver (#1130)Martin
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-04Add mkZero, mkOne and mkUmulo to bv utils. (#1200)Aina Niemetz
2017-10-04Ho quant util (#1119)Andrew Reynolds
2017-10-03Move sygus grammar utilities to separate file. (#1184)Andrew Reynolds
2017-10-02Unify hash functions for pairs (#1161)Andres Noetzli
2017-10-02Add 5 FP kinds for partial to total fn conversion (#1128)Martin
2017-10-02Address comments from PR #1164. (#1174)Mathias Preiner
2017-10-01Removing throw specifiers from TypeEnumeratorBase's operator* and isFinished....Tim King
2017-10-01CID 1457268: Initializing CegConjecture::d_syntax_guided to false. (#1181)Tim King
2017-10-01Refactor check function in last call effort of non-linear extension. (#1175)Andrew Reynolds
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-26Fix type checking of to_real (#1127)Martin Brain
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback