cvc5.git
2018-03-21 Mathias PreinerRefactor mkoptions (#1631)
2018-03-21 Aina NiemetzAdd bit-vector extract example. (#1681)
2018-03-21 Andrew ReynoldsMore rewrites for indexof (#1648)
2018-03-21 Andres Noetzli Move regression tests to single Makefile.am (#1658)
2018-03-21 Andres NoetzliFix various regression tests (#1657)
2018-03-21 Andrew ReynoldsFix for string disequality processing (#1679)
2018-03-20 Mathias PreinerAdd support for CaDiCaL as eager BV SAT solver. (#1675)
2018-03-20 Andrew ReynoldsMinor refactor datatypes sygus (#1673)
2018-03-20 Andrew ReynoldsInternally remove redundant assertions and infer equali...
2018-03-20 Andrew ReynoldsFix datatype dump regression. (#1672)
2018-03-20 Andrew ReynoldsMinor fix and addition to sygus sampler (#1678)
2018-03-20 Aina NiemetzAdd parameterized datatypes example. (#1676)
2018-03-20 yoni206correct instruction for running example (#1669)
2018-03-20 Andrew ReynoldsEnable CEGQI for non-linear (#1674)
2018-03-19 Andrew ReynoldsDocument inferences for strings (#1642)
2018-03-13 Mathias PreinerUse Cryptominisat version 5.0.2 (instead of 4.2.0)...
2018-03-13 Aina NiemetzSmtEngine::getModel() is now public. (#1665)
2018-03-09 Aina NiemetzPrinters are now managed as unique_ptr (fix mem leak...
2018-03-09 Aina NiemetzSome minor cleanup in bv::utils. (#1663)
2018-03-09 Aina NiemetzAdd support for SMT-LIB v2.5 command get-unsat-assumpti...
2018-03-09 Andres NoetzliSkip (get-unsat-assumptions) tests not supported (...
2018-03-09 Mathias PreinerCleanup Cryptominisat SAT wrapper. (#1652)
2018-03-09 Aina NiemetzFixed message in get-antlr script.
2018-03-09 Mathias PreinerFix Travis for unit test compilation errors. (#1651)
2018-03-07 Mathias PreinerMake statistics output consistent. (#1647)
2018-03-06 Andrew ReynoldsSimplify initialization of quantifiers engine (#1641)
2018-03-06 Andrew ReynoldsRefactor symmetry breaking in datatypes sygus (#1640)
2018-03-06 Andres NoetzliRemove printf from output utilities (#1629)
2018-03-06 Andrew ReynoldsUpdate semantics for string indexof and replace (#1630)
2018-03-05 Mathias PreinerFix boost url in contrib/get-win-dependencies.
2018-03-05 Mathias PreinerEnable -Wsuggest-override by default. (#1643)
2018-03-05 Andrew ReynoldsFix for sampler. (#1639)
2018-03-05 Aina NiemetzAdd support for check-sat-assuming. (#1637)
2018-03-05 Aina NiemetzAdd CVC4_PUBLIC keyword to overloads of << for Expr...
2018-03-05 Aina NiemetzAdd uniform way to serialize containers of Expr to...
2018-03-02 Aina NiemetzFixed typo.
2018-03-02 Andrew ReynoldsOptimization for sygus streaming mode (#1636)
2018-03-02 Andrew ReynoldsSimplify sygus wrt miniscoping (#1634)
2018-03-02 Aina NiemetzFixed comments in smt_engine.h.
2018-03-02 Andrew ReynoldsPrint candidate rewrites in terms of original grammar...
2018-03-02 Andrew ReynoldsCreate infrastructure for sygus modules (#1632)
2018-02-28 Aina NiemetzSmtEngine::getAssignment now returns a vector of assign...
2018-02-28 Andrew ReynoldsMinor fixes for rec-fun (#1616)
2018-02-28 Aina NiemetzRemove unused code in pushDefineFunRecScop in smt2...
2018-02-27 Andrew ReynoldsImprove rewriter for string indexof (#1592)
2018-02-27 Andrew ReynoldsOption to not use partial function semantics for arithm...
2018-02-27 Andrew ReynoldsImprovements to sygus sampling (#1621)
2018-02-24 Andres NoetzliAdd unit tests for BitVector, minor BV rewrite fix...
2018-02-23 Aina NiemetzSplit and document bitvector.h. (#1615)
2018-02-23 Andrew ReynoldsFix cd-simplification for strings (#1624)
2018-02-22 Andrew ReynoldsMinor improvements to string rewriter (#1572)
2018-02-22 Aina NiemetzFixed disabling the BV equality slicer for quantifiers...
2018-02-22 Aina NiemetzDisable BV equality slicer if not pure QF_BV. (#1619)
2018-02-20 Aina NiemetzImprove documentation of bv::utils::isCoreTerm (#1617)
2018-02-20 Aina NiemetzMoved and simplified bv::utils::intersect. (#1614)
2018-02-20 Andrew ReynoldsMinor fixes and additions for transcendental functions...
2018-02-20 Aina NiemetzUnrecursified and merged bv::utils::is(Core|Equality...
2018-02-17 Aina Niemetzbv::utils::mk(And|Or) Do not return true if size of...
2018-02-16 Aina NiemetzMake regress1 default, only test regress0 on Travis...
2018-02-16 Aina NiemetzRemoved bv::utils::mkConjunction (redundant). (#1610)
2018-02-15 Andrew ReynoldsFix corner case for rewrite of mult by pow 2 (#1601)
2018-02-15 Andrew ReynoldsRefactor regressions (#1581)
2018-02-15 Andres NoetzliFix context memory manager unit test (#1609)
2018-02-14 Andrew ReynoldsQuantifiers subdirectories (#1608)
2018-02-14 Andres NoetzliRemove unused cd_set_collection.h (#1606)
2018-02-14 Aina NiemetzProvide a uniform way to serialize node containers...
2018-02-13 Aina NiemetzMoved (unrecursified) bv::utils::collectVars. (#1602)
2018-02-13 Aina NiemetzSkip header for determining top contributors list....
2018-02-13 Andrew ReynoldsOption to use extended rewriter as a preprocessing...
2018-02-12 Andrew ReynoldsMinor improvements to sygus sampler (#1598)
2018-02-11 Aina NiemetzMove (unrecursified) bv::utils::numNodes to lazy_bitbla...
2018-02-11 Andrew ReynoldsMore minor improvements to synth-rr (#1597)
2018-02-10 Aina NiemetzMove BitVector specific funs from bv::utils to util...
2018-02-10 Aina NiemetzRemove mkNode from bv::utils (#1587)
2018-02-09 Tim KingRemoving an always true comparison (unsigned) >= 0u...
2018-02-09 Andrew ReynoldsClass to reduce printing of redundant candidate rewrite...
2018-02-09 Tim KingRenaming CHECK to CVC4_CHECK. This avoids name collisio...
2018-02-09 Tim KingReplacing an incorrect reference to an injected class...
2018-02-09 Andres NoetzliReplace CMM flag with debug CMM flag, fix leak in debug...
2018-02-09 Tim KingInlining line_buffered_input to avoid warning about...
2018-02-08 Aina NiemetzClean up bv utils (part one). (#1580)
2018-02-08 Tim KingAdding virtual destructors on classes with virtual...
2018-02-08 Andrew ReynoldsMinor improvements to sygus sampling. (#1577)
2018-02-08 Aina NiemetzUpdated copyright
2018-02-08 Tim KingInitializing Timer::d_wall_limit (CID 1362899). (#1573)
2018-02-08 Aina NiemetzSimplify and cleanup bv::utils::mkConjunction. (#1571)
2018-02-08 Mathias PreinerCheck whether Cryptominisat4/ABC was installed via...
2018-02-08 Andres NoetzliRemove invalid regression test (#1579)
2018-02-08 Tim KingRemoving an unused variable. (#1576)
2018-02-08 Tim KingFixing more inconsistent usages of override. (#1575)
2018-02-08 Aina NiemetzReduce number of Travis builds. (#1578)
2018-02-08 Tim KingFixing line numbers on type_checker_template.cpp (...
2018-02-07 Mathias PreinerCleanup Cryptominisat header. (#1561)
2018-02-07 Aina NiemetzUse template for bv::utils::mkOr. (#1570)
2018-02-07 Tim KingAdds a new CHECK macro that abort()s on failure. (...
2018-02-07 Andrew ReynoldsAdd remaining transcendental functions (#1551)
2018-02-07 Aina NiemetzUse template for bv::utils::mkAnd. (#1569)
2018-02-07 Aina NiemetzRenamed bv::utils::isBVGroundTerm to isBvConstTerm...
2018-02-07 Aina NiemetzSplit and document theory_bv_utils. (#1566)
2018-02-07 Mathias PreinerUse separate shell script for common get-* script parts...
next