cvc5.git
2018-04-23 Andrew ReynoldsDraft smt comp 2018 for quantifiers and non-linear...
2018-04-21 Andrew ReynoldsImprove sygus sampling for strings (#1802)
2018-04-21 Andres NoetzliRemove unused cache.h (#1795)
2018-04-20 yoni206Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv...
2018-04-20 Andrew Reynolds Reenable filtering based on ordering in sygus sampler...
2018-04-20 Andrew ReynoldsDraft of casc j9 scripts (#1800)
2018-04-20 yoni206Allow metadata lines in test files to have leading...
2018-04-20 PaulMengSymmetry detection module (#1749)
2018-04-20 Andres NoetzliRestrict test summary to first-level subfolders (#1797)
2018-04-19 yoni206Adding config/tap-driver.sh to .gitignore (#1792)
2018-04-19 Andres NoetzliRefactor pbRewrites preprocessing pass (#1767)
2018-04-19 Andres NoetzliRemove tap-driver.sh (#1791)
2018-04-17 Andres NoetzliAdd timeout (option) to regression script (#1786)
2018-04-17 Andres NoetzliDisable slow regression test (#1787)
2018-04-16 Andres NoetzliDisable check proofs/unsat cores for two regs (#1785)
2018-04-16 Andrew ReynoldsMake 256 the default cardinality for strings (#1783)
2018-04-16 Andres NoetzliRemoveTermFormulas: Remove ContainsTermITEVisitor ...
2018-04-16 Andrew ReynoldsSkolemize candidate rewrite rule checks (#1777)
2018-04-16 Andrew ReynoldsMake strings fmf apply to all but internally generated...
2018-04-15 Andrew ReynoldsFix type error with regexp (#1778)
2018-04-15 Andrew ReynoldsFix mk type const (#1776)
2018-04-14 Andrew ReynoldsAnother fix for sygus rr stats. (#1768)
2018-04-14 Andres Noetzli[Reg] Make status/unsat-core detection more robust...
2018-04-14 Andres NoetzliFix get-unsat-core detection in regression script ...
2018-04-14 yoni206allowing --bool-to-bv without quantifiers (#1771)
2018-04-14 Andres NoetzliFix use-after-free in eager bitblaster (#1772)
2018-04-14 Andrew ReynoldsDisable split for negative contains. (#1774)
2018-04-13 Andres NoetzliFix issue in regression script when proofs enabled...
2018-04-13 Andrew ReynoldsFix alpha equivalence for higher-order (#1769)
2018-04-12 Andrew ReynoldsFixes for free variables in assertions (#1762)
2018-04-11 Aina NiemetzRefactored BVGauss preprocessing pass. (#1766)
2018-04-11 Andrew ReynoldsProperly implement function extensionality based on...
2018-04-10 Andrew Reynolds Improve accuracy of stats for sygus sampler (#1755)
2018-04-10 Andres NoetzliRemove unused arith options (#1758)
2018-04-10 Andrew ReynoldsFix hasSubterm calls for higher-order (#1760)
2018-04-10 Aina NiemetzFix dumping of benchmark in SmtEngine::checkSatisfiabil...
2018-04-10 Andrew ReynoldsFix higher-order term indexing. (#1754)
2018-04-09 Andrew ReynoldsFix sygus substr static symmetry breaking (#1761)
2018-04-08 Andres NoetzliWarn about trailing spaces in src/Makefile.am (#1759)
2018-04-08 Andrew ReynoldsAllow predetermined first-order variables when construc...
2018-04-08 Andrew ReynoldsCheck free variables in assertions (#1737)
2018-04-08 Andrew ReynoldsDo not introduce uinterpreted constants in TPTP parser...
2018-04-08 Andrew ReynoldsAdd quantifier name attribute. (#1756)
2018-04-07 Aina NiemetzFixed get-authors.
2018-04-06 Arjun ViswanathanAdd define rec fun to cvc parser (#1738)
2018-04-06 Andres Noetzli Python regression script (#1662)
2018-04-05 Mathias PreinerAdd more general SignExtendUltConst rewriting. (#1385)
2018-04-05 Andres NoetzliMake Python bindings example compatible w/ Python3...
2018-04-05 Andres NoetzliUpdate README for regression tests (#1746)
2018-04-04 Andrew ReynoldsProper initialization and destruction of sygus unif...
2018-04-04 Andrew ReynoldsFix for corner case of higher-order matching (#1708)
2018-04-04 Andrew ReynoldsDo not debug check models when unknown (#1748)
2018-04-04 Andrew ReynoldsFix sygus infer (#1747)
2018-04-04 Andres NoetzliRefactor IntToBV preprocessing pass (#1716)
2018-04-04 Andrew ReynoldsOption to turn arbitrary input into sygus (#1704)
2018-04-04 Andres Noetzli[BVMiniSat] Avoid duplicates in conflicts (#1745)
2018-04-03 Andrew ReynoldsMake sygus unif I/O an subclass of sygus unif (#1741)
2018-04-03 Andrew ReynoldsUse choice when expanding definitions for inverse trans...
2018-04-03 Andrew ReynoldsInternal sygus type checking (#1734)
2018-04-03 Andrew ReynoldsImprovements to extended rewriter for Booleans and...
2018-04-02 Andrew ReynoldsMake sygus unif utility use sygus unif strategies ...
2018-04-02 yoni206a formula should be an instance of itself (#1668)
2018-04-02 Clark BarrettRemove references to nyu (#1721)
2018-04-02 Mathias PreinerReorganize bitblaster code. (#1695)
2018-04-02 yoni206Do not call toString() on malformed node when throwing...
2018-03-30 Andrew ReynoldsDisable regression (#1731)
2018-03-30 Andrew ReynoldsSplit strategy representation from SygusUnif (#1730)
2018-03-30 Andrew ReynoldsDo not use factoring inference for transcendental funct...
2018-03-29 Andrew ReynoldsSimplify sygus unif so that it is one-to-one with funct...
2018-03-27 Andrew ReynoldsMake sygus pbe use sygus unif utility (#1724)
2018-03-27 Andrew ReynoldsFix for --sygus-rr-synth (#1723)
2018-03-27 Andrew ReynoldsMake sygus unif utility (#1720)
2018-03-27 Andrew ReynoldsFilter candidate rewrites based on matching (#1682)
2018-03-27 Andres NoetzliBetter normalization of string concatenation (#1719)
2018-03-27 Andrew ReynoldsDocumentation and simplifications for PBE (#1677)
2018-03-26 Andres NoetzliRegression level 0 for distcheck on Travis (#1714)
2018-03-26 Andres NoetzliAdd support for filtering regressions with regex (...
2018-03-26 Andres NoetzliFix memory leak in bvminisat (#1710)
2018-03-26 Andres NoetzliMake Java bindings work with newer build envs (#1709)
2018-03-26 Andres Noetzli Add reasoning for inequalities in str rewriter (#1713)
2018-03-26 Andrew ReynoldsSynth-check and accelerate options for sygus-rr (#1691)
2018-03-26 Andrew ReynoldsAbort when sygus-verify finds unsoundness. (#1717)
2018-03-26 Andres NoetzliRewrites for substr of strings of length one (#1712)
2018-03-26 Andrew ReynoldsCheck model only when sat (#1694)
2018-03-25 Andrew ReynoldsCleanup various exit calls (#1692)
2018-03-25 Mathias PreinerRemove doc/libcvc4.3 from options/Makefile.am. (#1696)
2018-03-23 Andrew ReynoldsAdd a few quantifiers regressions to improve coverage...
2018-03-23 Andrew ReynoldsRemove abstract regular expression constant (#1698)
2018-03-23 Andrew ReynoldsRemove unused code (#1700)
2018-03-23 Andrew ReynoldsMinor reorganization for ematching (#1701)
2018-03-23 Andrew ReynoldsEnable post-condition strenghtening by default for...
2018-03-22 Mathias PreinerIgnore whitespaces and moved code for contrib/get-authors.
2018-03-21 Andres NoetzliFix 'make regress' (#1683)
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)
next