projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
only lazy trie changes (#1885)
[cvc5.git]
/
src
/
2018-05-08
Haniel Barbosa
only lazy trie changes (#1885)
tree
|
commitdiff
2018-05-07
Andrew Reynolds
Add support for str.code (#1821)
tree
|
commitdiff
2018-05-05
Andrew Reynolds
Fix handling of TO_REAL in cvc printer (#1876)
tree
|
commitdiff
2018-05-05
Andrew Reynolds
Remove special case for record selector printing. ...
tree
|
commitdiff
2018-05-04
Andrew Reynolds
Cegis unif register evaluation points (#1878)
tree
|
commitdiff
2018-05-04
Andres Noetzli
Make --output-lang consistent with --lang (#1877)
tree
|
commitdiff
2018-05-04
Andrew Reynolds
Do not print tuples. (#1874)
tree
|
commitdiff
2018-05-04
Mathias Preiner
Refactor bv-intro-pow2 preprocessing pass. (#1851)
tree
|
commitdiff
2018-05-04
Andres Noetzli
Fix printing of multiple datatypes (#1872)
tree
|
commitdiff
2018-05-04
Haniel Barbosa
Move Lazy trie datastructure to its own file (#1871)
tree
|
commitdiff
2018-05-04
Andrew Reynolds
Initialize cegis unif strategy (#1861)
tree
|
commitdiff
2018-05-04
Andrew Reynolds
Document datatypes sygus (#1818)
tree
|
commitdiff
2018-05-04
Andrew Reynolds
Sets subtypes (#1095)
tree
|
commitdiff
2018-05-03
Mathias Preiner
Fix redundant internalPush calls. (#1865)
tree
|
commitdiff
2018-05-03
Andres Noetzli
Fix warnings in proof code (#1850)
tree
|
commitdiff
2018-05-03
Andrew Reynolds
Interleave quantifiers checks with ground theory checks...
tree
|
commitdiff
2018-05-03
Andrew Reynolds
Option to interleave tangent plane inferences (#1833)
tree
|
commitdiff
2018-05-03
Andrew Reynolds
Link cegis unif with the enumeration manager (#1859)
tree
|
commitdiff
2018-05-03
Haniel Barbosa
Make CegisUnif default to Cegis when no unif used ...
tree
|
commitdiff
2018-05-03
Andrew Reynolds
Fix cvc printer for nullary constructors (#1856)
tree
|
commitdiff
2018-05-03
Andres Noetzli
Remove (dummy) SMT1 printer (#1854)
tree
|
commitdiff
2018-05-03
Andrew Reynolds
Support HORN logic string (#1849)
tree
|
commitdiff
2018-05-03
Andrew Reynolds
Initial support for string standard in smt lib 2.6...
tree
|
commitdiff
2018-05-01
Andrew Reynolds
Cegis unif enumerator manager (#1837)
tree
|
commitdiff
2018-05-01
Andrew Reynolds
Improve tangent planes for transcendental functions...
tree
|
commitdiff
2018-04-30
Haniel Barbosa
Refactor real2int (#1813)
tree
|
commitdiff
2018-04-30
Andres Noetzli
Remove dead code in bv-to-bool preprocessing pass ...
tree
|
commitdiff
2018-04-30
Andrew Reynolds
Remove subsort symmetry breaking (#1807)
tree
|
commitdiff
2018-04-30
Andrew Reynolds
Fix 1156 (#1830)
tree
|
commitdiff
2018-04-30
Andrew Reynolds
Allow multiple functions in sygus unif approaches ...
tree
|
commitdiff
2018-04-30
Andrew Reynolds
Make factoring inference more aggressive (#1825)
tree
|
commitdiff
2018-04-30
Andrew Reynolds
Refactor nonlinear check (#1814)
tree
|
commitdiff
2018-04-30
Andrew Reynolds
Improvements to simple transcendental function check...
tree
|
commitdiff
2018-04-28
Haniel Barbosa
Initial implementation of SygusUnifRL (#1829)
tree
|
commitdiff
2018-04-28
Andrew Reynolds
Make construct solution behavior specific to SygusIO...
tree
|
commitdiff
2018-04-27
Andrew Reynolds
Print function for equality status. (#1826)
tree
|
commitdiff
2018-04-27
Andrew Reynolds
Simplify tangent plane direction (#1824)
tree
|
commitdiff
2018-04-27
Haniel Barbosa
New module for synthesizing functions in a data-driven...
tree
|
commitdiff
2018-04-27
Andrew Reynolds
Core improvements to extended rewriter (#1820)
tree
|
commitdiff
2018-04-26
Andrew Reynolds
Fix subgoal generation context (#1816)
tree
|
commitdiff
2018-04-25
yoni206
Refactor array-proofs and uf-proofs (#1655)
tree
|
commitdiff
2018-04-25
Andrew Reynolds
Equality resolution in the extended rewriter (#1811)
tree
|
commitdiff
2018-04-25
yoni206
Refactor bv-to-bool and bool-to-bv preprocessing passes...
tree
|
commitdiff
2018-04-25
Andrew Reynolds
Move candidate rewrite code to own file (#1804)
tree
|
commitdiff
2018-04-25
Andrew Reynolds
Add benchmark requiring subgoal generation with inducti...
tree
|
commitdiff
2018-04-25
Andrew Reynolds
Remove nl solve subs option. (#1803)
tree
|
commitdiff
2018-04-25
Andrew Reynolds
Fix issue with multi-triggers that include variable...
tree
|
commitdiff
2018-04-21
Andrew Reynolds
Improve sygus sampling for strings (#1802)
tree
|
commitdiff
2018-04-21
Andres Noetzli
Remove unused cache.h (#1795)
tree
|
commitdiff
2018-04-20
yoni206
Enforcing --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
PaulMeng
Symmetry detection module (#1749)
tree
|
commitdiff
2018-04-19
Andres Noetzli
Refactor pbRewrites preprocessing pass (#1767)
tree
|
commitdiff
2018-04-16
Andrew Reynolds
Make 256 the default cardinality for strings (#1783)
tree
|
commitdiff
2018-04-16
Andres Noetzli
RemoveTermFormulas: Remove ContainsTermITEVisitor ...
tree
|
commitdiff
2018-04-16
Andrew Reynolds
Skolemize candidate rewrite rule checks (#1777)
tree
|
commitdiff
2018-04-16
Andrew Reynolds
Make strings fmf apply to all but internally generated...
tree
|
commitdiff
2018-04-15
Andrew Reynolds
Fix type error with regexp (#1778)
tree
|
commitdiff
2018-04-15
Andrew Reynolds
Fix mk type const (#1776)
tree
|
commitdiff
2018-04-14
Andrew Reynolds
Another fix for sygus rr stats. (#1768)
tree
|
commitdiff
2018-04-14
yoni206
allowing --bool-to-bv without quantifiers (#1771)
tree
|
commitdiff
2018-04-14
Andres Noetzli
Fix use-after-free in eager bitblaster (#1772)
tree
|
commitdiff
2018-04-14
Andrew Reynolds
Disable split for negative contains. (#1774)
tree
|
commitdiff
2018-04-13
Andrew Reynolds
Fix alpha equivalence for higher-order (#1769)
tree
|
commitdiff
2018-04-12
Andrew Reynolds
Fixes for free variables in assertions (#1762)
tree
|
commitdiff
2018-04-11
Aina Niemetz
Refactored BVGauss preprocessing pass. (#1766)
tree
|
commitdiff
2018-04-11
Andrew Reynolds
Properly 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 Noetzli
Remove unused arith options (#1758)
tree
|
commitdiff
2018-04-10
Andrew Reynolds
Fix hasSubterm calls for higher-order (#1760)
tree
|
commitdiff
2018-04-10
Aina Niemetz
Fix dumping of benchmark in SmtEngine::checkSatisfiabil...
tree
|
commitdiff
2018-04-10
Andrew Reynolds
Fix higher-order term indexing. (#1754)
tree
|
commitdiff
2018-04-09
Andrew Reynolds
Fix sygus substr static symmetry breaking (#1761)
tree
|
commitdiff
2018-04-08
Andrew Reynolds
Allow predetermined first-order variables when construc...
tree
|
commitdiff
2018-04-08
Andrew Reynolds
Check free variables in assertions (#1737)
tree
|
commitdiff
2018-04-08
Andrew Reynolds
Do not introduce uinterpreted constants in TPTP parser...
tree
|
commitdiff
2018-04-08
Andrew Reynolds
Add quantifier name attribute. (#1756)
tree
|
commitdiff
2018-04-06
Arjun Viswanathan
Add define rec fun to cvc parser (#1738)
tree
|
commitdiff
2018-04-05
Mathias Preiner
Add more general SignExtendUltConst rewriting. (#1385)
tree
|
commitdiff
2018-04-04
Andrew Reynolds
Proper initialization and destruction of sygus unif...
tree
|
commitdiff
2018-04-04
Andrew Reynolds
Fix for corner case of higher-order matching (#1708)
tree
|
commitdiff
2018-04-04
Andrew Reynolds
Do not debug check models when unknown (#1748)
tree
|
commitdiff
2018-04-04
Andrew Reynolds
Fix sygus infer (#1747)
tree
|
commitdiff
2018-04-04
Andres Noetzli
Refactor IntToBV preprocessing pass (#1716)
tree
|
commitdiff
2018-04-04
Andrew Reynolds
Option 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 Reynolds
Make sygus unif I/O an subclass of sygus unif (#1741)
tree
|
commitdiff
2018-04-03
Andrew Reynolds
Use choice when expanding definitions for inverse trans...
tree
|
commitdiff
2018-04-03
Andrew Reynolds
Internal sygus type checking (#1734)
tree
|
commitdiff
2018-04-03
Andrew Reynolds
Improvements to extended rewriter for Booleans and...
tree
|
commitdiff
2018-04-02
Andrew Reynolds
Make sygus unif utility use sygus unif strategies ...
tree
|
commitdiff
2018-04-02
Clark Barrett
Remove references to nyu (#1721)
tree
|
commitdiff
2018-04-02
Mathias Preiner
Reorganize bitblaster code. (#1695)
tree
|
commitdiff
2018-04-02
yoni206
Do not call toString() on malformed node when throwing...
tree
|
commitdiff
2018-03-30
Andrew Reynolds
Split strategy representation from SygusUnif (#1730)
tree
|
commitdiff
2018-03-30
Andrew Reynolds
Do not use factoring inference for transcendental funct...
tree
|
commitdiff
2018-03-29
Andrew Reynolds
Simplify sygus unif so that it is one-to-one with funct...
tree
|
commitdiff
2018-03-27
Andrew Reynolds
Make sygus pbe use sygus unif utility (#1724)
tree
|
commitdiff
2018-03-27
Andrew Reynolds
Fix for --sygus-rr-synth (#1723)
tree
|
commitdiff
2018-03-27
Andrew Reynolds
Make sygus unif utility (#1720)
tree
|
commitdiff
next