projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2018-01-04 Tim KingRemoving throw specifiers from context/. (#1473) commit | commitdiff | tree
2018-01-03 Aina NiemetzAdd side conditions for UGT/SGT over BITVECTOR_UREM... commit | commitdiff | tree
2018-01-03 Mathias PreinerAdd UGT/SGT side conditions for LSHR. (#1469) commit | commitdiff | tree
2018-01-03 Aina Niemetz Add side conditions for inequalities over BITVECTOR_MU... commit | commitdiff | tree
2018-01-03 Andrew ReynoldsGlobal negate (#1466) commit | commitdiff | tree
2018-01-03 Mathias Preiner Add side conditions for inequalities of ASHR. (#1461) commit | commitdiff | tree
2018-01-03 Aina NiemetzAdd side conditions for inequalities over BITVECTOR_UDI... commit | commitdiff | tree
2018-01-03 Aina NiemetzSimplify side condition for SGE over UREM (index =... commit | commitdiff | tree
2018-01-03 Mathias PreinerFix handling for UGT/SGT. (#1467) commit | commitdiff | tree
2018-01-02 Andrew ReynoldsRewrites for BitVector multiplication (#1465) commit | commitdiff | tree
2018-01-02 Mathias PreinerAdd side conditions for inequalities of LSHR. (#1462) commit | commitdiff | tree
2018-01-02 Andrew ReynoldsImprove rewriter for string equality (#1427) commit | commitdiff | tree
2017-12-30 Aina NiemetzAdd side conditions for inequalities over BITVECTOR_URE... commit | commitdiff | tree
2017-12-30 Aina NiemetzFix RNG for seed = 0. (#1459) commit | commitdiff | tree
2017-12-30 Andrew ReynoldsCbqi repeat solve literal (#1458) commit | commitdiff | tree
2017-12-29 Mathias PreinerAdd side conditions for inequalities of AND/OR. (#1457) commit | commitdiff | tree
2017-12-29 Aina NiemetzFix unit tests for ineq for CBQI BV. (#1456) commit | commitdiff | tree
2017-12-29 Aina NiemetzAdd unit tests for side conditions for inequality for... commit | commitdiff | tree
2017-12-28 Andrew ReynoldsFixes for cbqi (#1453) commit | commitdiff | tree
2017-12-28 Arjun ViswanathanRel smt parser (#1446) commit | commitdiff | tree
2017-12-28 Aina NiemetzMinor refactor for inequality handling for CBQI BV... commit | commitdiff | tree
2017-12-27 Andrew ReynoldsDisable sygus PBE when sygus stream is enabled (#1451) commit | commitdiff | tree
2017-12-21 Andrew ReynoldsFixes for cbqi-bv (#1449) commit | commitdiff | tree
2017-12-21 Aina NiemetzAdd explicit disequality handling when generating side... commit | commitdiff | tree
2017-12-21 Mathias PreinerAdd rewriting rule for ranking benchmarks. (#1448) commit | commitdiff | tree
2017-12-20 Andrew ReynoldsTranscendental functions check model (#1443) commit | commitdiff | tree
2017-12-19 Aina NiemetzFix travis write errors. (#1445) commit | commitdiff | tree
2017-12-16 Aina NiemetzEnable side condition handling for shifts introduced... commit | commitdiff | tree
2017-12-14 Aina NiemetzAdd missing side conditions for SHL, LSHR, ASHR for... commit | commitdiff | tree
2017-12-12 Mathias PreinerAdd SIGTERM handler. (#1440) commit | commitdiff | tree
2017-12-11 justinxu421Add new infrastructure for preprocessing passes (#1053) commit | commitdiff | tree
2017-12-10 Andrew ReynoldsFix issue 1433. (#1435) commit | commitdiff | tree
2017-12-10 Andres NoetzliFix issue with mkConst/getConst of TypeConstant (#1439) commit | commitdiff | tree
2017-12-09 Mathias PreinerAdd CEGQI BV linearization of additions and equalities... commit | commitdiff | tree
2017-12-08 Aina NiemetzFixed side conditions for CBQI BV, added unit tests... commit | commitdiff | tree
2017-12-08 Andrew ReynoldsDocument and clean datatypes rewriter (#1437) commit | commitdiff | tree
2017-12-08 Andrew ReynoldsMake collect model info return a Bool (#1421) commit | commitdiff | tree
2017-12-07 Andrew ReynoldsFixes related to SyGuS + real arithmetic (#1432) commit | commitdiff | tree
2017-12-07 Andrew ReynoldsAdd command for define-fun-rec and add to API (#1412) commit | commitdiff | tree
2017-12-06 Aina NiemetzFixed time stats for MiniSat solve time. (#1431) commit | commitdiff | tree
2017-12-06 Andres NoetzliRemove CDChunkList (#1414) commit | commitdiff | tree
2017-12-05 Mathias PreinerFix output of --show-trace-tags. (#1430) commit | commitdiff | tree
2017-12-05 Haniel BarbosaAdding SyGuS grammars for rationals. (#1426) commit | commitdiff | tree
2017-12-04 Andrew ReynoldsEliminate expand definitions from Sygus (#1425) commit | commitdiff | tree
2017-12-04 Andrew ReynoldsFix strings rewriter for strip constant endpoint revers... commit | commitdiff | tree
2017-12-04 Mathias PreinerFix side condition for BITVECTOR_MULT. (#1422) commit | commitdiff | tree
2017-12-03 Haniel BarbosaNormalize grammars - 2 (#1420) commit | commitdiff | tree
2017-12-02 Andrew ReynoldsMinor improvements to inst match generator (#1415) commit | commitdiff | tree
2017-12-02 Andrew ReynoldsImprove rewriter for string replace (#1416) commit | commitdiff | tree
2017-12-01 Andres NoetzliFix reset-assertions (#1413) commit | commitdiff | tree
2017-12-01 Andrew ReynoldsMinor additions for sygus (#1419) commit | commitdiff | tree
2017-12-01 Andrew ReynoldsRefactor and generalize PBE strategies (#1410) commit | commitdiff | tree
2017-12-01 Andres NoetzliFix build when Valgrind instrumentation enabled commit | commitdiff | tree
2017-12-01 Andres NoetzliAdd debugging tools for ContextMemoryManager (#1407) commit | commitdiff | tree
2017-11-30 Aina NiemetzAdd Gaussian Elimination as a preprocessing pass for... commit | commitdiff | tree
2017-11-30 Andrew ReynoldsFixes for issue 1404 (#1409) commit | commitdiff | tree
2017-11-30 Andrew ReynoldsRemove remaining references to QuantArith (#1408) commit | commitdiff | tree
2017-11-30 Andrew ReynoldsMinor improvements and changes to defaults for cbqi... commit | commitdiff | tree
2017-11-29 Andrew ReynoldsImprove caching in term formula removal (#1398) commit | commitdiff | tree
2017-11-29 Tim KingAdding missing break statements. CID 1362756. (#1394) commit | commitdiff | tree
2017-11-29 Tim KingSimplifying the conditions in checkLetBinding to avoid... commit | commitdiff | tree
2017-11-29 Mathias PreinerAdd Cryptominisat script and patches to source file... commit | commitdiff | tree
2017-11-29 Andrew ReynoldsImprove the rewriter for SINE. (#1221) commit | commitdiff | tree
2017-11-28 Andrew ReynoldsImprove rewrite for string substr (#1337) commit | commitdiff | tree
2017-11-28 Andrew ReynoldsImprove trigger filter instances (#1402) commit | commitdiff | tree
2017-11-28 Tim KingRemoving throw specifiers from internal Printer hierarc... commit | commitdiff | tree
2017-11-28 Andrew ReynoldsFix models for --solve-real-as-int. (#1371) commit | commitdiff | tree
2017-11-25 Andrew ReynoldsFixes for higher-order (#1405) commit | commitdiff | tree
2017-11-25 Andrew Reynolds(Refactor) Instantiate utility (#1387) commit | commitdiff | tree
2017-11-24 Andrew ReynoldsImplement tangent and secant planes for transcendental... commit | commitdiff | tree
2017-11-24 Andrew ReynoldsHo parsing and regressions (#1350) commit | commitdiff | tree
2017-11-23 Haniel BarbosaConverting defined functions and let expressions from... commit | commitdiff | tree
2017-11-22 Andrew ReynoldsSygus Lambda Grammars (#1390) commit | commitdiff | tree
2017-11-22 Andrew ReynoldsTranscendental tangent planes utilities (#1288) commit | commitdiff | tree
2017-11-21 Haniel BarbosaAdding infrastructure for normalizing SyGuS grammars... commit | commitdiff | tree
2017-11-21 Andrew ReynoldsCegqi bv remove extract terms preprocess pass (#1376) commit | commitdiff | tree
2017-11-20 Tim KingInitializes members of QuantInfo. Resolves CID 1362929... commit | commitdiff | tree
2017-11-20 Tim KingRemoving an unused variable from SygusInput. Resolves... commit | commitdiff | tree
2017-11-19 Andrew ReynoldsHo instantiation (#1204) commit | commitdiff | tree
2017-11-19 Tim KingNames the Effort enum of QuantConflictFind class. ... commit | commitdiff | tree
2017-11-17 Andrew Reynolds(Refactor) Document and clean single invocation partiti... commit | commitdiff | tree
2017-11-17 Aina NiemetzAdd random number generator. (#1370) commit | commitdiff | tree
2017-11-16 Andrew Reynolds(Refactor) Arithmetic monomial sum (#1381) commit | commitdiff | tree
2017-11-16 Tim KingInitializes BitVectorProof::d_isAssumptionConflict... commit | commitdiff | tree
2017-11-15 Andrew ReynoldsSygus print callbacks (#1348) commit | commitdiff | tree
2017-11-15 Andrew ReynoldsReenable some regressions, minor. (#1369) commit | commitdiff | tree
2017-11-15 Tim KingRemoves an unused variable from Theory. (#1375) commit | commitdiff | tree
2017-11-15 Tim KingInitializing members of Datatype. Addresses CIDs 136289... commit | commitdiff | tree
2017-11-15 Tim KingAdding garbage collection for Proof objects. (#1294) commit | commitdiff | tree
2017-11-15 Andrew ReynoldsMake QEffort an enum (#1366) commit | commitdiff | tree
2017-11-14 Andrew Reynolds(Refactor) Split sygus term db (#1335) commit | commitdiff | tree
2017-11-14 Andrew ReynoldsClean Ceg Instantiators (#1365) commit | commitdiff | tree
2017-11-14 Tim KingCleaning up exporting vectors within commands. Resolves... commit | commitdiff | tree
2017-11-14 Tim KingInitializes InstPropagator::d_has_relevant_inst. Resolv... commit | commitdiff | tree
2017-11-14 Tim KingInitializes RegExpOpr::d_char_start and d_char_end... commit | commitdiff | tree
2017-11-14 Tim KingInitializes TriggerInfo::polarity. Resolves CID 1172054... commit | commitdiff | tree
2017-11-14 Tim KingInitializes NodeTheoryPair::timestamp in the default... commit | commitdiff | tree
2017-11-14 Andrew Reynolds(Refactor) Decouple rep set iterator and quantifiers... commit | commitdiff | tree
2017-11-13 Tim KingInitializing SharedTermsDatabase::d_conflictPolarity... commit | commitdiff | tree
2017-11-13 Andrew ReynoldsDisable sygus qe preprocessing by default (#1353) commit | commitdiff | tree
next