projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Piecing solutions together in CegisUnif (#1894)
[cvc5.git] / src /
2018-05-09 Haniel BarbosaPiecing solutions together in CegisUnif (#1894) tree | commitdiff
2018-05-09 yoni206Reorder class members in bv-to-bool and bool-to-bv... tree | commitdiff
2018-05-09 Andrew ReynoldsBetter option names for PBE (#1891) tree | commitdiff
2018-05-09 Andrew ReynoldsMake symmetry-breaker-exp into a preprocessing pass... tree | commitdiff
2018-05-09 PaulMengAdd the symmetry breaker module (#1847) tree | commitdiff
2018-05-08 Mathias PreinerRefactor bv-abstraction preprocessing pass. (#1860) tree | commitdiff
2018-05-08 Andrew ReynoldsInfrastructure for approximations in model output ... tree | commitdiff
2018-05-08 Andrew ReynoldsSupport for str.<= and str.< (#1882) tree | commitdiff
2018-05-08 Aina NiemetzFix order of preprocessing pass registration. (#1887) tree | commitdiff
2018-05-08 Haniel BarbosaClassifying data in SygusUnifRL (#1886) tree | commitdiff
2018-05-08 Andrew ReynoldsInfrastructure for CEGQI handled status (#1873) tree | commitdiff
2018-05-08 Haniel Barbosaonly lazy trie changes (#1885) tree | commitdiff
2018-05-07 Andrew ReynoldsAdd support for str.code (#1821) tree | commitdiff
2018-05-05 Andrew ReynoldsFix handling of TO_REAL in cvc printer (#1876) tree | commitdiff
2018-05-05 Andrew ReynoldsRemove special case for record selector printing. ... tree | commitdiff
2018-05-04 Andrew ReynoldsCegis unif register evaluation points (#1878) tree | commitdiff
2018-05-04 Andres NoetzliMake --output-lang consistent with --lang (#1877) tree | commitdiff
2018-05-04 Andrew ReynoldsDo not print tuples. (#1874) tree | commitdiff
2018-05-04 Mathias PreinerRefactor bv-intro-pow2 preprocessing pass. (#1851) tree | commitdiff
2018-05-04 Andres NoetzliFix printing of multiple datatypes (#1872) tree | commitdiff
2018-05-04 Haniel BarbosaMove Lazy trie datastructure to its own file (#1871) tree | commitdiff
2018-05-04 Andrew ReynoldsInitialize cegis unif strategy (#1861) tree | commitdiff
2018-05-04 Andrew ReynoldsDocument datatypes sygus (#1818) tree | commitdiff
2018-05-04 Andrew ReynoldsSets subtypes (#1095) tree | commitdiff
2018-05-03 Mathias PreinerFix redundant internalPush calls. (#1865) tree | commitdiff
2018-05-03 Andres NoetzliFix warnings in proof code (#1850) tree | commitdiff
2018-05-03 Andrew ReynoldsInterleave quantifiers checks with ground theory checks... tree | commitdiff
2018-05-03 Andrew ReynoldsOption to interleave tangent plane inferences (#1833) tree | commitdiff
2018-05-03 Andrew ReynoldsLink cegis unif with the enumeration manager (#1859) tree | commitdiff
2018-05-03 Haniel BarbosaMake CegisUnif default to Cegis when no unif used ... tree | commitdiff
2018-05-03 Andrew ReynoldsFix cvc printer for nullary constructors (#1856) tree | commitdiff
2018-05-03 Andres NoetzliRemove (dummy) SMT1 printer (#1854) tree | commitdiff
2018-05-03 Andrew ReynoldsSupport HORN logic string (#1849) tree | commitdiff
2018-05-03 Andrew ReynoldsInitial support for string standard in smt lib 2.6... tree | commitdiff
2018-05-01 Andrew ReynoldsCegis unif enumerator manager (#1837) tree | commitdiff
2018-05-01 Andrew ReynoldsImprove tangent planes for transcendental functions... tree | commitdiff
2018-04-30 Haniel BarbosaRefactor real2int (#1813) tree | commitdiff
2018-04-30 Andres NoetzliRemove dead code in bv-to-bool preprocessing pass ... tree | commitdiff
2018-04-30 Andrew ReynoldsRemove subsort symmetry breaking (#1807) tree | commitdiff
2018-04-30 Andrew ReynoldsFix 1156 (#1830) tree | commitdiff
2018-04-30 Andrew ReynoldsAllow multiple functions in sygus unif approaches ... tree | commitdiff
2018-04-30 Andrew ReynoldsMake factoring inference more aggressive (#1825) tree | commitdiff
2018-04-30 Andrew ReynoldsRefactor nonlinear check (#1814) tree | commitdiff
2018-04-30 Andrew ReynoldsImprovements to simple transcendental function check... tree | commitdiff
2018-04-28 Haniel BarbosaInitial implementation of SygusUnifRL (#1829) tree | commitdiff
2018-04-28 Andrew ReynoldsMake construct solution behavior specific to SygusIO... tree | commitdiff
2018-04-27 Andrew ReynoldsPrint function for equality status. (#1826) tree | commitdiff
2018-04-27 Andrew ReynoldsSimplify tangent plane direction (#1824) tree | commitdiff
2018-04-27 Haniel BarbosaNew module for synthesizing functions in a data-driven... tree | commitdiff
2018-04-27 Andrew ReynoldsCore improvements to extended rewriter (#1820) tree | commitdiff
2018-04-26 Andrew ReynoldsFix subgoal generation context (#1816) tree | commitdiff
2018-04-25 yoni206Refactor array-proofs and uf-proofs (#1655) tree | commitdiff
2018-04-25 Andrew ReynoldsEquality resolution in the extended rewriter (#1811) tree | commitdiff
2018-04-25 yoni206Refactor bv-to-bool and bool-to-bv preprocessing passes... tree | commitdiff
2018-04-25 Andrew ReynoldsMove candidate rewrite code to own file (#1804) tree | commitdiff
2018-04-25 Andrew ReynoldsAdd benchmark requiring subgoal generation with inducti... tree | commitdiff
2018-04-25 Andrew ReynoldsRemove nl solve subs option. (#1803) tree | commitdiff
2018-04-25 Andrew ReynoldsFix issue with multi-triggers that include variable... tree | commitdiff
2018-04-21 Andrew ReynoldsImprove sygus sampling for strings (#1802) tree | commitdiff
2018-04-21 Andres NoetzliRemove unused cache.h (#1795) tree | commitdiff
2018-04-20 yoni206Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv... tree | commitdiff
2018-04-20 Andrew Reynolds Reenable filtering based on ordering in sygus sampler... tree | commitdiff
2018-04-20 PaulMengSymmetry detection module (#1749) tree | commitdiff
2018-04-19 Andres NoetzliRefactor pbRewrites preprocessing pass (#1767) tree | commitdiff
2018-04-16 Andrew ReynoldsMake 256 the default cardinality for strings (#1783) tree | commitdiff
2018-04-16 Andres NoetzliRemoveTermFormulas: Remove ContainsTermITEVisitor ... tree | commitdiff
2018-04-16 Andrew ReynoldsSkolemize candidate rewrite rule checks (#1777) tree | commitdiff
2018-04-16 Andrew ReynoldsMake strings fmf apply to all but internally generated... tree | commitdiff
2018-04-15 Andrew ReynoldsFix type error with regexp (#1778) tree | commitdiff
2018-04-15 Andrew ReynoldsFix mk type const (#1776) tree | commitdiff
2018-04-14 Andrew ReynoldsAnother fix for sygus rr stats. (#1768) tree | commitdiff
2018-04-14 yoni206allowing --bool-to-bv without quantifiers (#1771) tree | commitdiff
2018-04-14 Andres NoetzliFix use-after-free in eager bitblaster (#1772) tree | commitdiff
2018-04-14 Andrew ReynoldsDisable split for negative contains. (#1774) tree | commitdiff
2018-04-13 Andrew ReynoldsFix alpha equivalence for higher-order (#1769) tree | commitdiff
2018-04-12 Andrew ReynoldsFixes for free variables in assertions (#1762) tree | commitdiff
2018-04-11 Aina NiemetzRefactored BVGauss preprocessing pass. (#1766) tree | commitdiff
2018-04-11 Andrew ReynoldsProperly implement function extensionality based on... tree | commitdiff
2018-04-10 Andrew Reynolds Improve accuracy of stats for sygus sampler (#1755) tree | commitdiff
2018-04-10 Andres NoetzliRemove unused arith options (#1758) tree | commitdiff
2018-04-10 Andrew ReynoldsFix hasSubterm calls for higher-order (#1760) tree | commitdiff
2018-04-10 Aina NiemetzFix dumping of benchmark in SmtEngine::checkSatisfiabil... tree | commitdiff
2018-04-10 Andrew ReynoldsFix higher-order term indexing. (#1754) tree | commitdiff
2018-04-09 Andrew ReynoldsFix sygus substr static symmetry breaking (#1761) tree | commitdiff
2018-04-08 Andrew ReynoldsAllow predetermined first-order variables when construc... tree | commitdiff
2018-04-08 Andrew ReynoldsCheck free variables in assertions (#1737) tree | commitdiff
2018-04-08 Andrew ReynoldsDo not introduce uinterpreted constants in TPTP parser... tree | commitdiff
2018-04-08 Andrew ReynoldsAdd quantifier name attribute. (#1756) tree | commitdiff
2018-04-06 Arjun ViswanathanAdd define rec fun to cvc parser (#1738) tree | commitdiff
2018-04-05 Mathias PreinerAdd more general SignExtendUltConst rewriting. (#1385) tree | commitdiff
2018-04-04 Andrew ReynoldsProper initialization and destruction of sygus unif... tree | commitdiff
2018-04-04 Andrew ReynoldsFix for corner case of higher-order matching (#1708) tree | commitdiff
2018-04-04 Andrew ReynoldsDo not debug check models when unknown (#1748) tree | commitdiff
2018-04-04 Andrew ReynoldsFix sygus infer (#1747) tree | commitdiff
2018-04-04 Andres NoetzliRefactor IntToBV preprocessing pass (#1716) tree | commitdiff
2018-04-04 Andrew ReynoldsOption to turn arbitrary input into sygus (#1704) tree | commitdiff
2018-04-04 Andres Noetzli[BVMiniSat] Avoid duplicates in conflicts (#1745) tree | commitdiff
2018-04-03 Andrew ReynoldsMake sygus unif I/O an subclass of sygus unif (#1741) tree | commitdiff
2018-04-03 Andrew ReynoldsUse choice when expanding definitions for inverse trans... tree | commitdiff
2018-04-03 Andrew ReynoldsInternal sygus type checking (#1734) tree | commitdiff
next