projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2018-04-14 Andrew ReynoldsAnother fix for sygus rr stats. (#1768) commit | commitdiff | tree
2018-04-14 Andres Noetzli[Reg] Make status/unsat-core detection more robust... commit | commitdiff | tree
2018-04-14 Andres NoetzliFix get-unsat-core detection in regression script ... commit | commitdiff | tree
2018-04-14 yoni206allowing --bool-to-bv without quantifiers (#1771) commit | commitdiff | tree
2018-04-14 Andres NoetzliFix use-after-free in eager bitblaster (#1772) commit | commitdiff | tree
2018-04-14 Andrew ReynoldsDisable split for negative contains. (#1774) commit | commitdiff | tree
2018-04-13 Andres NoetzliFix issue in regression script when proofs enabled... commit | commitdiff | tree
2018-04-13 Andrew ReynoldsFix alpha equivalence for higher-order (#1769) commit | commitdiff | tree
2018-04-12 Andrew ReynoldsFixes for free variables in assertions (#1762) commit | commitdiff | tree
2018-04-11 Aina NiemetzRefactored BVGauss preprocessing pass. (#1766) commit | commitdiff | tree
2018-04-11 Andrew ReynoldsProperly implement function extensionality based on... commit | commitdiff | tree
2018-04-10 Andrew Reynolds Improve accuracy of stats for sygus sampler (#1755) commit | commitdiff | tree
2018-04-10 Andres NoetzliRemove unused arith options (#1758) commit | commitdiff | tree
2018-04-10 Andrew ReynoldsFix hasSubterm calls for higher-order (#1760) commit | commitdiff | tree
2018-04-10 Aina NiemetzFix dumping of benchmark in SmtEngine::checkSatisfiabil... commit | commitdiff | tree
2018-04-10 Andrew ReynoldsFix higher-order term indexing. (#1754) commit | commitdiff | tree
2018-04-09 Andrew ReynoldsFix sygus substr static symmetry breaking (#1761) commit | commitdiff | tree
2018-04-08 Andres NoetzliWarn about trailing spaces in src/Makefile.am (#1759) commit | commitdiff | tree
2018-04-08 Andrew ReynoldsAllow predetermined first-order variables when construc... commit | commitdiff | tree
2018-04-08 Andrew ReynoldsCheck free variables in assertions (#1737) commit | commitdiff | tree
2018-04-08 Andrew ReynoldsDo not introduce uinterpreted constants in TPTP parser... commit | commitdiff | tree
2018-04-08 Andrew ReynoldsAdd quantifier name attribute. (#1756) commit | commitdiff | tree
2018-04-07 Aina NiemetzFixed get-authors. commit | commitdiff | tree
2018-04-06 Arjun ViswanathanAdd define rec fun to cvc parser (#1738) commit | commitdiff | tree
2018-04-06 Andres Noetzli Python regression script (#1662) commit | commitdiff | tree
2018-04-05 Mathias PreinerAdd more general SignExtendUltConst rewriting. (#1385) commit | commitdiff | tree
2018-04-05 Andres NoetzliMake Python bindings example compatible w/ Python3... commit | commitdiff | tree
2018-04-05 Andres NoetzliUpdate README for regression tests (#1746) commit | commitdiff | tree
2018-04-04 Andrew ReynoldsProper initialization and destruction of sygus unif... commit | commitdiff | tree
2018-04-04 Andrew ReynoldsFix for corner case of higher-order matching (#1708) commit | commitdiff | tree
2018-04-04 Andrew ReynoldsDo not debug check models when unknown (#1748) commit | commitdiff | tree
2018-04-04 Andrew ReynoldsFix sygus infer (#1747) commit | commitdiff | tree
2018-04-04 Andres NoetzliRefactor IntToBV preprocessing pass (#1716) commit | commitdiff | tree
2018-04-04 Andrew ReynoldsOption to turn arbitrary input into sygus (#1704) commit | commitdiff | tree
2018-04-04 Andres Noetzli[BVMiniSat] Avoid duplicates in conflicts (#1745) commit | commitdiff | tree
2018-04-03 Andrew ReynoldsMake sygus unif I/O an subclass of sygus unif (#1741) commit | commitdiff | tree
2018-04-03 Andrew ReynoldsUse choice when expanding definitions for inverse trans... commit | commitdiff | tree
2018-04-03 Andrew ReynoldsInternal sygus type checking (#1734) commit | commitdiff | tree
2018-04-03 Andrew ReynoldsImprovements to extended rewriter for Booleans and... commit | commitdiff | tree
2018-04-02 Andrew ReynoldsMake sygus unif utility use sygus unif strategies ... commit | commitdiff | tree
2018-04-02 yoni206a formula should be an instance of itself (#1668) commit | commitdiff | tree
2018-04-02 Clark BarrettRemove references to nyu (#1721) commit | commitdiff | tree
2018-04-02 Mathias PreinerReorganize bitblaster code. (#1695) commit | commitdiff | tree
2018-04-02 yoni206Do not call toString() on malformed node when throwing... commit | commitdiff | tree
2018-03-30 Andrew ReynoldsDisable regression (#1731) commit | commitdiff | tree
2018-03-30 Andrew ReynoldsSplit strategy representation from SygusUnif (#1730) commit | commitdiff | tree
2018-03-30 Andrew ReynoldsDo not use factoring inference for transcendental funct... commit | commitdiff | tree
2018-03-29 Andrew ReynoldsSimplify sygus unif so that it is one-to-one with funct... commit | commitdiff | tree
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
next