projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2018-05-01 Andrew ReynoldsCegis unif enumerator manager (#1837) commit | commitdiff | tree
2018-05-01 Andrew ReynoldsImprove tangent planes for transcendental functions... commit | commitdiff | tree
2018-04-30 Haniel BarbosaRefactor real2int (#1813) commit | commitdiff | tree
2018-04-30 Andres NoetzliRemove dead code in bv-to-bool preprocessing pass ... commit | commitdiff | tree
2018-04-30 Andrew ReynoldsRemove subsort symmetry breaking (#1807) commit | commitdiff | tree
2018-04-30 Andrew ReynoldsFix 1156 (#1830) commit | commitdiff | tree
2018-04-30 Andres NoetzliDisable unsat-cores/proofs for slow regression (#1835) commit | commitdiff | tree
2018-04-30 Andrew ReynoldsAllow multiple functions in sygus unif approaches ... commit | commitdiff | tree
2018-04-30 Andrew ReynoldsMake factoring inference more aggressive (#1825) commit | commitdiff | tree
2018-04-30 Andrew ReynoldsRefactor nonlinear check (#1814) commit | commitdiff | tree
2018-04-30 Andrew ReynoldsImprovements to simple transcendental function check... commit | commitdiff | tree
2018-04-28 Haniel BarbosaInitial implementation of SygusUnifRL (#1829) commit | commitdiff | tree
2018-04-28 Andrew ReynoldsMake construct solution behavior specific to SygusIO... commit | commitdiff | tree
2018-04-27 Andrew ReynoldsPrint function for equality status. (#1826) commit | commitdiff | tree
2018-04-27 Andrew ReynoldsSimplify tangent plane direction (#1824) commit | commitdiff | tree
2018-04-27 Haniel BarbosaNew module for synthesizing functions in a data-driven... commit | commitdiff | tree
2018-04-27 Andrew ReynoldsCore improvements to extended rewriter (#1820) commit | commitdiff | tree
2018-04-26 Andrew ReynoldsFix subgoal generation context (#1816) commit | commitdiff | tree
2018-04-25 yoni206Refactor array-proofs and uf-proofs (#1655) commit | commitdiff | tree
2018-04-25 Andrew ReynoldsEquality resolution in the extended rewriter (#1811) commit | commitdiff | tree
2018-04-25 yoni206Refactor bv-to-bool and bool-to-bv preprocessing passes... commit | commitdiff | tree
2018-04-25 Andrew ReynoldsMove candidate rewrite code to own file (#1804) commit | commitdiff | tree
2018-04-25 Andrew ReynoldsAdd benchmark requiring subgoal generation with inducti... commit | commitdiff | tree
2018-04-25 Andrew ReynoldsRemove nl solve subs option. (#1803) commit | commitdiff | tree
2018-04-25 Andrew ReynoldsFix issue with multi-triggers that include variable... commit | commitdiff | tree
2018-04-23 Andrew ReynoldsDraft smt comp 2018 for quantifiers and non-linear... commit | commitdiff | tree
2018-04-21 Andrew ReynoldsImprove sygus sampling for strings (#1802) commit | commitdiff | tree
2018-04-21 Andres NoetzliRemove unused cache.h (#1795) commit | commitdiff | tree
2018-04-20 yoni206Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv... commit | commitdiff | tree
2018-04-20 Andrew Reynolds Reenable filtering based on ordering in sygus sampler... commit | commitdiff | tree
2018-04-20 Andrew ReynoldsDraft of casc j9 scripts (#1800) commit | commitdiff | tree
2018-04-20 yoni206Allow metadata lines in test files to have leading... commit | commitdiff | tree
2018-04-20 PaulMengSymmetry detection module (#1749) commit | commitdiff | tree
2018-04-20 Andres NoetzliRestrict test summary to first-level subfolders (#1797) commit | commitdiff | tree
2018-04-19 yoni206Adding config/tap-driver.sh to .gitignore (#1792) commit | commitdiff | tree
2018-04-19 Andres NoetzliRefactor pbRewrites preprocessing pass (#1767) commit | commitdiff | tree
2018-04-19 Andres NoetzliRemove tap-driver.sh (#1791) commit | commitdiff | tree
2018-04-17 Andres NoetzliAdd timeout (option) to regression script (#1786) commit | commitdiff | tree
2018-04-17 Andres NoetzliDisable slow regression test (#1787) commit | commitdiff | tree
2018-04-16 Andres NoetzliDisable check proofs/unsat cores for two regs (#1785) commit | commitdiff | tree
2018-04-16 Andrew ReynoldsMake 256 the default cardinality for strings (#1783) commit | commitdiff | tree
2018-04-16 Andres NoetzliRemoveTermFormulas: Remove ContainsTermITEVisitor ... commit | commitdiff | tree
2018-04-16 Andrew ReynoldsSkolemize candidate rewrite rule checks (#1777) commit | commitdiff | tree
2018-04-16 Andrew ReynoldsMake strings fmf apply to all but internally generated... commit | commitdiff | tree
2018-04-15 Andrew ReynoldsFix type error with regexp (#1778) commit | commitdiff | tree
2018-04-15 Andrew ReynoldsFix mk type const (#1776) commit | commitdiff | tree
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
next