summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2017-11-22Transcendental tangent planes utilities (#1288)Andrew Reynolds
2017-11-21Adding infrastructure for normalizing SyGuS grammars (#1397)Haniel Barbosa
2017-11-21Cegqi bv remove extract terms preprocess pass (#1376)Andrew Reynolds
2017-11-20Initializes members of QuantInfo. Resolves CID 1362929. (#1391)Tim King
2017-11-19Removing an unused variable from SygusInput. Resolves CID 1362932. (#1392)Tim King
2017-11-18Ho instantiation (#1204)Andrew Reynolds
2017-11-18Names the Effort enum of QuantConflictFind class. (#1354)Tim King
2017-11-17(Refactor) Document and clean single invocation partition. (#1364)Andrew Reynolds
2017-11-17Add random number generator. (#1370)Aina Niemetz
2017-11-16(Refactor) Arithmetic monomial sum (#1381)Andrew Reynolds
2017-11-15Initializes BitVectorProof::d_isAssumptionConflict. Resolves CID 1362898. (#1...Tim King
2017-11-15Sygus print callbacks (#1348)Andrew Reynolds
2017-11-15Removes an unused variable from Theory. (#1375)Tim King
2017-11-15Initializing members of Datatype. Addresses CIDs 1362897, 1362912, 1362923 an...Tim King
2017-11-15Adding garbage collection for Proof objects. (#1294)Tim King
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-14Cleaning up exporting vectors within commands. Resolves CID 1172285 and 11722...Tim King
2017-11-14Initializes InstPropagator::d_has_relevant_inst. Resolves 1362891. (#1360)Tim King
2017-11-13Initializes RegExpOpr::d_char_start and d_char_end. (#1359)Tim King
2017-11-13Initializes TriggerInfo::polarity. Resolves CID 1172054. (#1358)Tim King
2017-11-13Initializes NodeTheoryPair::timestamp in the default constructor. (#1356)Tim King
2017-11-13(Refactor) Decouple rep set iterator and quantifiers (#1339)Andrew Reynolds
2017-11-13Initializing SharedTermsDatabase::d_conflictPolarity. Resolves 1172045. (#1355)Tim King
2017-11-13Disable sygus qe preprocessing by default (#1353)Andrew Reynolds
2017-11-13Implement enumerator for functions. (#1243)Andrew Reynolds
2017-11-13Argument Relevance for Synthesis Conjectures (#1311)Andrew Reynolds
2017-11-13Initializes CegConjectureSingleInvSol::d_root_id. (#1361)Tim King
2017-11-13Initializing SortInference::initialSortCount. Resolves 1172053. (#1357)Tim King
2017-11-10(Documentation-only) datatype.h (#1346)Andrew Reynolds
2017-11-10Printing for higher-order (#1347)Andrew Reynolds
2017-11-09Higher-order prep (#1338)Andrew Reynolds
2017-11-09 Decouple sygus term database and term database. (#1317)Andrew Reynolds
2017-11-09Add modular arithmetic operators. (#1321)Aina Niemetz
2017-11-07Initializing QModelBuilder members. (#1334)Tim King
2017-11-07Combining d_conflictHasBeenRaised and d_conflictIndex into a CDMaybe. (#1332)Tim King
2017-11-07Initializing TrailHashMap::d_uniqueKeys. (#1331)Tim King
2017-11-07 Initialize TimerStat::d_start. (#1330)Tim King
2017-11-07Initializing Smt1::d_logic in all cases. This was resolved by extending the L...Tim King
2017-11-07Guard relevant domain computation properly, minor. (#1325)Andrew Reynolds
2017-11-07 Removing an unused member from Tptp. Initializing members of Tptp. (#1326)Tim King
2017-11-07Moving the enum ArithType to partial_model. Adding a new type Unset in the en...Tim King
2017-11-07Allow FORALL in quantifier elimination command (#1322)Andrew Reynolds
2017-11-07Initializing EquivSygusInvarianceTest::d_conj in the constructor. (#1327)Tim King
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-06Add getValue() for Rational and Integer (GMP and CLN). (#1309)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback