projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2018-03-27 Andrew ReynoldsMake sygus pbe use sygus unif utility (#1724) commit | commitdiff | tree
2018-03-27 Andrew ReynoldsFix for --sygus-rr-synth (#1723) commit | commitdiff | tree
2018-03-27 Andrew ReynoldsMake sygus unif utility (#1720) commit | commitdiff | tree
2018-03-27 Andrew ReynoldsFilter candidate rewrites based on matching (#1682) commit | commitdiff | tree
2018-03-27 Andres NoetzliBetter normalization of string concatenation (#1719) commit | commitdiff | tree
2018-03-27 Andrew ReynoldsDocumentation and simplifications for PBE (#1677) commit | commitdiff | tree
2018-03-26 Andres NoetzliRegression level 0 for distcheck on Travis (#1714) commit | commitdiff | tree
2018-03-26 Andres NoetzliAdd support for filtering regressions with regex (... commit | commitdiff | tree
2018-03-26 Andres NoetzliFix memory leak in bvminisat (#1710) commit | commitdiff | tree
2018-03-26 Andres NoetzliMake Java bindings work with newer build envs (#1709) commit | commitdiff | tree
2018-03-26 Andres Noetzli Add reasoning for inequalities in str rewriter (#1713) commit | commitdiff | tree
2018-03-26 Andrew ReynoldsSynth-check and accelerate options for sygus-rr (#1691) commit | commitdiff | tree
2018-03-26 Andrew ReynoldsAbort when sygus-verify finds unsoundness. (#1717) commit | commitdiff | tree
2018-03-26 Andres NoetzliRewrites for substr of strings of length one (#1712) commit | commitdiff | tree
2018-03-26 Andrew ReynoldsCheck model only when sat (#1694) commit | commitdiff | tree
2018-03-25 Andrew ReynoldsCleanup various exit calls (#1692) commit | commitdiff | tree
2018-03-25 Mathias PreinerRemove doc/libcvc4.3 from options/Makefile.am. (#1696) commit | commitdiff | tree
2018-03-23 Andrew ReynoldsAdd a few quantifiers regressions to improve coverage... commit | commitdiff | tree
2018-03-23 Andrew ReynoldsRemove abstract regular expression constant (#1698) commit | commitdiff | tree
2018-03-23 Andrew ReynoldsRemove unused code (#1700) commit | commitdiff | tree
2018-03-23 Andrew ReynoldsMinor reorganization for ematching (#1701) commit | commitdiff | tree
2018-03-23 Andrew ReynoldsEnable post-condition strenghtening by default for... commit | commitdiff | tree
2018-03-22 Mathias PreinerIgnore whitespaces and moved code for contrib/get-authors. commit | commitdiff | tree
2018-03-21 Andres NoetzliFix 'make regress' (#1683) commit | commitdiff | tree
2018-03-21 Mathias PreinerRefactor mkoptions (#1631) commit | commitdiff | tree
2018-03-21 Aina NiemetzAdd bit-vector extract example. (#1681) commit | commitdiff | tree
2018-03-21 Andrew ReynoldsMore rewrites for indexof (#1648) commit | commitdiff | tree
2018-03-21 Andres Noetzli Move regression tests to single Makefile.am (#1658) commit | commitdiff | tree
2018-03-21 Andres NoetzliFix various regression tests (#1657) commit | commitdiff | tree
2018-03-21 Andrew ReynoldsFix for string disequality processing (#1679) commit | commitdiff | tree
2018-03-20 Mathias PreinerAdd support for CaDiCaL as eager BV SAT solver. (#1675) commit | commitdiff | tree
2018-03-20 Andrew ReynoldsMinor refactor datatypes sygus (#1673) commit | commitdiff | tree
2018-03-20 Andrew ReynoldsInternally remove redundant assertions and infer equali... commit | commitdiff | tree
2018-03-20 Andrew ReynoldsFix datatype dump regression. (#1672) commit | commitdiff | tree
2018-03-20 Andrew ReynoldsMinor fix and addition to sygus sampler (#1678) commit | commitdiff | tree
2018-03-20 Aina NiemetzAdd parameterized datatypes example. (#1676) commit | commitdiff | tree
2018-03-20 yoni206correct instruction for running example (#1669) commit | commitdiff | tree
2018-03-20 Andrew ReynoldsEnable CEGQI for non-linear (#1674) commit | commitdiff | tree
2018-03-19 Andrew ReynoldsDocument inferences for strings (#1642) commit | commitdiff | tree
2018-03-13 Mathias PreinerUse Cryptominisat version 5.0.2 (instead of 4.2.0)... commit | commitdiff | tree
2018-03-13 Aina NiemetzSmtEngine::getModel() is now public. (#1665) commit | commitdiff | tree
2018-03-09 Aina NiemetzPrinters are now managed as unique_ptr (fix mem leak... commit | commitdiff | tree
2018-03-09 Aina NiemetzSome minor cleanup in bv::utils. (#1663) commit | commitdiff | tree
2018-03-09 Aina NiemetzAdd support for SMT-LIB v2.5 command get-unsat-assumpti... commit | commitdiff | tree
2018-03-09 Andres NoetzliSkip (get-unsat-assumptions) tests not supported (... commit | commitdiff | tree
2018-03-09 Mathias PreinerCleanup Cryptominisat SAT wrapper. (#1652) commit | commitdiff | tree
2018-03-09 Aina NiemetzFixed message in get-antlr script. commit | commitdiff | tree
2018-03-09 Mathias PreinerFix Travis for unit test compilation errors. (#1651) commit | commitdiff | tree
2018-03-07 Mathias PreinerMake statistics output consistent. (#1647) commit | commitdiff | tree
2018-03-06 Andrew ReynoldsSimplify initialization of quantifiers engine (#1641) commit | commitdiff | tree
2018-03-06 Andrew ReynoldsRefactor symmetry breaking in datatypes sygus (#1640) commit | commitdiff | tree
2018-03-06 Andres NoetzliRemove printf from output utilities (#1629) commit | commitdiff | tree
2018-03-06 Andrew ReynoldsUpdate semantics for string indexof and replace (#1630) commit | commitdiff | tree
2018-03-05 Mathias PreinerFix boost url in contrib/get-win-dependencies. commit | commitdiff | tree
2018-03-05 Mathias PreinerEnable -Wsuggest-override by default. (#1643) commit | commitdiff | tree
2018-03-05 Andrew ReynoldsFix for sampler. (#1639) commit | commitdiff | tree
2018-03-05 Aina NiemetzAdd support for check-sat-assuming. (#1637) commit | commitdiff | tree
2018-03-05 Aina NiemetzAdd CVC4_PUBLIC keyword to overloads of << for Expr... commit | commitdiff | tree
2018-03-05 Aina NiemetzAdd uniform way to serialize containers of Expr to... commit | commitdiff | tree
2018-03-02 Aina NiemetzFixed typo. commit | commitdiff | tree
2018-03-02 Andrew ReynoldsOptimization for sygus streaming mode (#1636) commit | commitdiff | tree
2018-03-02 Andrew ReynoldsSimplify sygus wrt miniscoping (#1634) commit | commitdiff | tree
2018-03-02 Aina NiemetzFixed comments in smt_engine.h. commit | commitdiff | tree
2018-03-02 Andrew ReynoldsPrint candidate rewrites in terms of original grammar... commit | commitdiff | tree
2018-03-02 Andrew ReynoldsCreate infrastructure for sygus modules (#1632) commit | commitdiff | tree
2018-02-28 Aina NiemetzSmtEngine::getAssignment now returns a vector of assign... commit | commitdiff | tree
2018-02-28 Andrew ReynoldsMinor fixes for rec-fun (#1616) commit | commitdiff | tree
2018-02-28 Aina NiemetzRemove unused code in pushDefineFunRecScop in smt2... commit | commitdiff | tree
2018-02-27 Andrew ReynoldsImprove rewriter for string indexof (#1592) commit | commitdiff | tree
2018-02-27 Andrew ReynoldsOption to not use partial function semantics for arithm... commit | commitdiff | tree
2018-02-27 Andrew ReynoldsImprovements to sygus sampling (#1621) commit | commitdiff | tree
2018-02-24 Andres NoetzliAdd unit tests for BitVector, minor BV rewrite fix... commit | commitdiff | tree
2018-02-23 Aina NiemetzSplit and document bitvector.h. (#1615) commit | commitdiff | tree
2018-02-23 Andrew ReynoldsFix cd-simplification for strings (#1624) commit | commitdiff | tree
2018-02-22 Andrew ReynoldsMinor improvements to string rewriter (#1572) commit | commitdiff | tree
2018-02-22 Aina NiemetzFixed disabling the BV equality slicer for quantifiers... commit | commitdiff | tree
2018-02-22 Aina NiemetzDisable BV equality slicer if not pure QF_BV. (#1619) commit | commitdiff | tree
2018-02-20 Aina NiemetzImprove documentation of bv::utils::isCoreTerm (#1617) commit | commitdiff | tree
2018-02-20 Aina NiemetzMoved and simplified bv::utils::intersect. (#1614) commit | commitdiff | tree
2018-02-20 Andrew ReynoldsMinor fixes and additions for transcendental functions... commit | commitdiff | tree
2018-02-20 Aina NiemetzUnrecursified and merged bv::utils::is(Core|Equality... commit | commitdiff | tree
2018-02-17 Aina Niemetzbv::utils::mk(And|Or) Do not return true if size of... commit | commitdiff | tree
2018-02-16 Aina NiemetzMake regress1 default, only test regress0 on Travis... commit | commitdiff | tree
2018-02-16 Aina NiemetzRemoved bv::utils::mkConjunction (redundant). (#1610) commit | commitdiff | tree
2018-02-15 Andrew ReynoldsFix corner case for rewrite of mult by pow 2 (#1601) commit | commitdiff | tree
2018-02-15 Andrew ReynoldsRefactor regressions (#1581) commit | commitdiff | tree
2018-02-15 Andres NoetzliFix context memory manager unit test (#1609) commit | commitdiff | tree
2018-02-14 Andrew ReynoldsQuantifiers subdirectories (#1608) commit | commitdiff | tree
2018-02-14 Andres NoetzliRemove unused cd_set_collection.h (#1606) commit | commitdiff | tree
2018-02-14 Aina NiemetzProvide a uniform way to serialize node containers... commit | commitdiff | tree
2018-02-13 Aina NiemetzMoved (unrecursified) bv::utils::collectVars. (#1602) commit | commitdiff | tree
2018-02-13 Aina NiemetzSkip header for determining top contributors list.... commit | commitdiff | tree
2018-02-13 Andrew ReynoldsOption to use extended rewriter as a preprocessing... commit | commitdiff | tree
2018-02-12 Andrew ReynoldsMinor improvements to sygus sampler (#1598) commit | commitdiff | tree
2018-02-11 Aina NiemetzMove (unrecursified) bv::utils::numNodes to lazy_bitbla... commit | commitdiff | tree
2018-02-11 Andrew ReynoldsMore minor improvements to synth-rr (#1597) commit | commitdiff | tree
2018-02-10 Aina NiemetzMove BitVector specific funs from bv::utils to util... commit | commitdiff | tree
2018-02-10 Aina NiemetzRemove mkNode from bv::utils (#1587) commit | commitdiff | tree
2018-02-09 Tim KingRemoving an always true comparison (unsigned) >= 0u... commit | commitdiff | tree
2018-02-09 Andrew ReynoldsClass to reduce printing of redundant candidate rewrite... commit | commitdiff | tree
next