projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Removing more miscellaneous throw specifiers. (#1488)
[cvc5.git] / src /
2018-01-09 Tim KingRemoving more miscellaneous throw specifiers. (#1488) tree | commitdiff
2018-01-09 Aina NiemetzAdd bv util mkConst(unsigned, Integer&). (#1499) tree | commitdiff
2018-01-09 Tim KingRemove throw specifiers from symbol table. (#1490) tree | commitdiff
2018-01-09 Aina NiemetzAdded division by constant handling for CBQI BV. (... tree | commitdiff
2018-01-08 Tim KingRemoves throw specifiers from command.{h,cpp}. (#1485) tree | commitdiff
2018-01-08 Andrew ReynoldsImprovements to quant+BV/Bool variable elimination... tree | commitdiff
2018-01-08 Tim KingRemove throw specifiers from datatype. (#1489) tree | commitdiff
2018-01-08 Tim KingRe-ordering field initialization in QuantInfo to remove... tree | commitdiff
2018-01-08 Tim KingRemoves RationalFromDoubleException. Replaces this... tree | commitdiff
2018-01-06 Tim KingRemoving throw specifiers from src/parser/. (#1486) tree | commitdiff
2018-01-06 Mathias PreinerAdd special {SGE,SGT,NE}_UDIV1 side conditions for... tree | commitdiff
2018-01-06 Mathias PreinerUse simpler EQUAL SCs for LSHR0, LSHR1, ASHR0, AHSR1... tree | commitdiff
2018-01-05 Mathias PreinerAdd UGT/SGT side conditions for AND/OR + other fixes... tree | commitdiff
2018-01-05 Aina NiemetzFix side condition handling for PLUS, XOR, SIGN_EXTEND... tree | commitdiff
2018-01-05 Mathias PreinerAdd side conditions for inequalities of SHL. (#1472) tree | commitdiff
2018-01-04 Andrew ReynoldsImprovements for CBQI (#1478) tree | commitdiff
2018-01-04 Tim KingRemoving miscellaneous throw specifiers. (#1474) tree | commitdiff
2018-01-04 Tim KingRemoving throw specifiers from context/. (#1473) tree | commitdiff
2018-01-03 Aina NiemetzAdd side conditions for UGT/SGT over BITVECTOR_UREM... tree | commitdiff
2018-01-03 Mathias PreinerAdd UGT/SGT side conditions for LSHR. (#1469) tree | commitdiff
2018-01-03 Aina Niemetz Add side conditions for inequalities over BITVECTOR_MU... tree | commitdiff
2018-01-03 Andrew ReynoldsGlobal negate (#1466) tree | commitdiff
2018-01-03 Mathias Preiner Add side conditions for inequalities of ASHR. (#1461) tree | commitdiff
2018-01-03 Aina NiemetzAdd side conditions for inequalities over BITVECTOR_UDI... tree | commitdiff
2018-01-03 Aina NiemetzSimplify side condition for SGE over UREM (index =... tree | commitdiff
2018-01-03 Mathias PreinerFix handling for UGT/SGT. (#1467) tree | commitdiff
2018-01-02 Andrew ReynoldsRewrites for BitVector multiplication (#1465) tree | commitdiff
2018-01-02 Mathias PreinerAdd side conditions for inequalities of LSHR. (#1462) tree | commitdiff
2018-01-02 Andrew ReynoldsImprove rewriter for string equality (#1427) tree | commitdiff
2017-12-30 Aina NiemetzAdd side conditions for inequalities over BITVECTOR_URE... tree | commitdiff
2017-12-30 Aina NiemetzFix RNG for seed = 0. (#1459) tree | commitdiff
2017-12-30 Andrew ReynoldsCbqi repeat solve literal (#1458) tree | commitdiff
2017-12-29 Mathias PreinerAdd side conditions for inequalities of AND/OR. (#1457) tree | commitdiff
2017-12-29 Aina NiemetzAdd unit tests for side conditions for inequality for... tree | commitdiff
2017-12-28 Andrew ReynoldsFixes for cbqi (#1453) tree | commitdiff
2017-12-28 Arjun ViswanathanRel smt parser (#1446) tree | commitdiff
2017-12-28 Aina NiemetzMinor refactor for inequality handling for CBQI BV... tree | commitdiff
2017-12-27 Andrew ReynoldsDisable sygus PBE when sygus stream is enabled (#1451) tree | commitdiff
2017-12-21 Andrew ReynoldsFixes for cbqi-bv (#1449) tree | commitdiff
2017-12-21 Aina NiemetzAdd explicit disequality handling when generating side... tree | commitdiff
2017-12-21 Mathias PreinerAdd rewriting rule for ranking benchmarks. (#1448) tree | commitdiff
2017-12-20 Andrew ReynoldsTranscendental functions check model (#1443) tree | commitdiff
2017-12-16 Aina NiemetzEnable side condition handling for shifts introduced... tree | commitdiff
2017-12-14 Aina NiemetzAdd missing side conditions for SHL, LSHR, ASHR for... tree | commitdiff
2017-12-12 Mathias PreinerAdd SIGTERM handler. (#1440) tree | commitdiff
2017-12-11 justinxu421Add new infrastructure for preprocessing passes (#1053) tree | commitdiff
2017-12-10 Andrew ReynoldsFix issue 1433. (#1435) tree | commitdiff
2017-12-10 Andres NoetzliFix issue with mkConst/getConst of TypeConstant (#1439) tree | commitdiff
2017-12-09 Mathias PreinerAdd CEGQI BV linearization of additions and equalities... tree | commitdiff
2017-12-08 Aina NiemetzFixed side conditions for CBQI BV, added unit tests... tree | commitdiff
2017-12-08 Andrew ReynoldsDocument and clean datatypes rewriter (#1437) tree | commitdiff
2017-12-08 Andrew ReynoldsMake collect model info return a Bool (#1421) tree | commitdiff
2017-12-07 Andrew ReynoldsFixes related to SyGuS + real arithmetic (#1432) tree | commitdiff
2017-12-07 Andrew ReynoldsAdd command for define-fun-rec and add to API (#1412) tree | commitdiff
2017-12-06 Aina NiemetzFixed time stats for MiniSat solve time. (#1431) tree | commitdiff
2017-12-06 Andres NoetzliRemove CDChunkList (#1414) tree | commitdiff
2017-12-05 Mathias PreinerFix output of --show-trace-tags. (#1430) tree | commitdiff
2017-12-05 Haniel BarbosaAdding SyGuS grammars for rationals. (#1426) tree | commitdiff
2017-12-04 Andrew ReynoldsEliminate expand definitions from Sygus (#1425) tree | commitdiff
2017-12-04 Andrew ReynoldsFix strings rewriter for strip constant endpoint revers... tree | commitdiff
2017-12-04 Mathias PreinerFix side condition for BITVECTOR_MULT. (#1422) tree | commitdiff
2017-12-03 Haniel BarbosaNormalize grammars - 2 (#1420) tree | commitdiff
2017-12-02 Andrew ReynoldsMinor improvements to inst match generator (#1415) tree | commitdiff
2017-12-02 Andrew ReynoldsImprove rewriter for string replace (#1416) tree | commitdiff
2017-12-01 Andres NoetzliFix reset-assertions (#1413) tree | commitdiff
2017-12-01 Andrew ReynoldsMinor additions for sygus (#1419) tree | commitdiff
2017-12-01 Andrew ReynoldsRefactor and generalize PBE strategies (#1410) tree | commitdiff
2017-12-01 Andres NoetzliFix build when Valgrind instrumentation enabled tree | commitdiff
2017-12-01 Andres NoetzliAdd debugging tools for ContextMemoryManager (#1407) tree | commitdiff
2017-11-30 Aina NiemetzAdd Gaussian Elimination as a preprocessing pass for... tree | commitdiff
2017-11-30 Andrew ReynoldsFixes for issue 1404 (#1409) tree | commitdiff
2017-11-30 Andrew ReynoldsRemove remaining references to QuantArith (#1408) tree | commitdiff
2017-11-30 Andrew ReynoldsMinor improvements and changes to defaults for cbqi... tree | commitdiff
2017-11-29 Andrew ReynoldsImprove caching in term formula removal (#1398) tree | commitdiff
2017-11-29 Tim KingAdding missing break statements. CID 1362756. (#1394) tree | commitdiff
2017-11-29 Tim KingSimplifying the conditions in checkLetBinding to avoid... tree | commitdiff
2017-11-29 Andrew ReynoldsImprove the rewriter for SINE. (#1221) tree | commitdiff
2017-11-28 Andrew ReynoldsImprove rewrite for string substr (#1337) tree | commitdiff
2017-11-28 Andrew ReynoldsImprove trigger filter instances (#1402) tree | commitdiff
2017-11-28 Tim KingRemoving throw specifiers from internal Printer hierarc... tree | commitdiff
2017-11-28 Andrew ReynoldsFix models for --solve-real-as-int. (#1371) tree | commitdiff
2017-11-25 Andrew ReynoldsFixes for higher-order (#1405) tree | commitdiff
2017-11-25 Andrew Reynolds(Refactor) Instantiate utility (#1387) tree | commitdiff
2017-11-24 Andrew ReynoldsImplement tangent and secant planes for transcendental... tree | commitdiff
2017-11-24 Andrew ReynoldsHo parsing and regressions (#1350) tree | commitdiff
2017-11-23 Haniel BarbosaConverting defined functions and let expressions from... tree | commitdiff
2017-11-22 Andrew ReynoldsSygus Lambda Grammars (#1390) tree | commitdiff
2017-11-22 Andrew ReynoldsTranscendental tangent planes utilities (#1288) tree | commitdiff
2017-11-21 Haniel BarbosaAdding infrastructure for normalizing SyGuS grammars... tree | commitdiff
2017-11-21 Andrew ReynoldsCegqi bv remove extract terms preprocess pass (#1376) tree | commitdiff
2017-11-20 Tim KingInitializes members of QuantInfo. Resolves CID 1362929... tree | commitdiff
2017-11-20 Tim KingRemoving an unused variable from SygusInput. Resolves... tree | commitdiff
2017-11-19 Andrew ReynoldsHo instantiation (#1204) tree | commitdiff
2017-11-19 Tim KingNames the Effort enum of QuantConflictFind class. ... tree | commitdiff
2017-11-17 Andrew Reynolds(Refactor) Document and clean single invocation partiti... tree | commitdiff
2017-11-17 Aina NiemetzAdd random number generator. (#1370) tree | commitdiff
2017-11-16 Andrew Reynolds(Refactor) Arithmetic monomial sum (#1381) tree | commitdiff
2017-11-16 Tim KingInitializes BitVectorProof::d_isAssumptionConflict... tree | commitdiff
2017-11-15 Andrew ReynoldsSygus print callbacks (#1348) tree | commitdiff
2017-11-15 Tim KingRemoves an unused variable from Theory. (#1375) tree | commitdiff
next