projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Exclude Boolean connectives from ITE conditions in SygusUnifStrat (#1900)
[cvc5.git]
/
test
/
2018-05-10
Andrew Reynolds
Sygus repair constants (#1812)
tree
|
commitdiff
2018-05-09
Andrew Reynolds
Make symmetry-breaker-exp into a preprocessing pass...
tree
|
commitdiff
2018-05-08
Mathias Preiner
Refactor bv-abstraction preprocessing pass. (#1860)
tree
|
commitdiff
2018-05-08
Andrew Reynolds
Support for str.<= and str.< (#1882)
tree
|
commitdiff
2018-05-07
Andrew Reynolds
Add support for str.code (#1821)
tree
|
commitdiff
2018-05-04
Mathias Preiner
Refactor bv-intro-pow2 preprocessing pass. (#1851)
tree
|
commitdiff
2018-05-04
Andrew Reynolds
Sets subtypes (#1095)
tree
|
commitdiff
2018-05-03
Andrew Reynolds
Interleave quantifiers checks with ground theory checks...
tree
|
commitdiff
2018-05-03
Andrew Reynolds
Initial support for string standard in smt lib 2.6...
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
Disable unsat-cores/proofs for slow regression (#1835)
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-25
yoni206
Refactor bv-to-bool and bool-to-bv preprocessing passes...
tree
|
commitdiff
2018-04-25
Andrew Reynolds
Add benchmark requiring subgoal generation with inducti...
tree
|
commitdiff
2018-04-25
Andrew Reynolds
Fix issue with multi-triggers that include variable...
tree
|
commitdiff
2018-04-20
yoni206
Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv...
tree
|
commitdiff
2018-04-20
yoni206
Allow metadata lines in test files to have leading...
tree
|
commitdiff
2018-04-20
PaulMeng
Symmetry detection module (#1749)
tree
|
commitdiff
2018-04-20
Andres Noetzli
Restrict test summary to first-level subfolders (#1797)
tree
|
commitdiff
2018-04-19
Andres Noetzli
Refactor pbRewrites preprocessing pass (#1767)
tree
|
commitdiff
2018-04-17
Andres Noetzli
Add timeout (option) to regression script (#1786)
tree
|
commitdiff
2018-04-17
Andres Noetzli
Disable slow regression test (#1787)
tree
|
commitdiff
2018-04-16
Andres Noetzli
Disable check proofs/unsat cores for two regs (#1785)
tree
|
commitdiff
2018-04-14
Andres Noetzli
[Reg] Make status/unsat-core detection more robust...
tree
|
commitdiff
2018-04-14
Andres Noetzli
Fix get-unsat-core detection in regression script ...
tree
|
commitdiff
2018-04-13
Andres Noetzli
Fix issue in regression script when proofs enabled...
tree
|
commitdiff
2018-04-13
Andrew Reynolds
Fix alpha equivalence for higher-order (#1769)
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
Fix hasSubterm calls for higher-order (#1760)
tree
|
commitdiff
2018-04-10
Andrew Reynolds
Fix higher-order term indexing. (#1754)
tree
|
commitdiff
2018-04-06
Arjun Viswanathan
Add define rec fun to cvc parser (#1738)
tree
|
commitdiff
2018-04-06
Andres Noetzli
Python regression script (#1662)
tree
|
commitdiff
2018-04-05
Andres Noetzli
Update README for regression tests (#1746)
tree
|
commitdiff
2018-04-04
Andrew Reynolds
Fix for corner case of higher-order matching (#1708)
tree
|
commitdiff
2018-04-04
Andrew Reynolds
Option to turn arbitrary input into sygus (#1704)
tree
|
commitdiff
2018-04-03
Andrew Reynolds
Use choice when expanding definitions for inverse trans...
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-03-30
Andrew Reynolds
Disable regression (#1731)
tree
|
commitdiff
2018-03-27
Andres Noetzli
Better normalization of string concatenation (#1719)
tree
|
commitdiff
2018-03-26
Andres Noetzli
Add support for filtering regressions with regex (...
tree
|
commitdiff
2018-03-26
Andres Noetzli
Add reasoning for inequalities in str rewriter (#1713)
tree
|
commitdiff
2018-03-26
Andres Noetzli
Rewrites for substr of strings of length one (#1712)
tree
|
commitdiff
2018-03-23
Andrew Reynolds
Add a few quantifiers regressions to improve coverage...
tree
|
commitdiff
2018-03-21
Andres Noetzli
Fix 'make regress' (#1683)
tree
|
commitdiff
2018-03-21
Mathias Preiner
Refactor mkoptions (#1631)
tree
|
commitdiff
2018-03-21
Andres Noetzli
Move regression tests to single Makefile.am (#1658)
tree
|
commitdiff
2018-03-21
Andres Noetzli
Fix various regression tests (#1657)
tree
|
commitdiff
2018-03-21
Andrew Reynolds
Fix for string disequality processing (#1679)
tree
|
commitdiff
2018-03-20
Andrew Reynolds
Internally remove redundant assertions and infer equali...
tree
|
commitdiff
2018-03-20
Andrew Reynolds
Fix datatype dump regression. (#1672)
tree
|
commitdiff
2018-03-20
Andrew Reynolds
Enable CEGQI for non-linear (#1674)
tree
|
commitdiff
2018-03-09
Aina Niemetz
Add support for SMT-LIB v2.5 command get-unsat-assumpti...
tree
|
commitdiff
2018-03-09
Andres Noetzli
Skip (get-unsat-assumptions) tests not supported (...
tree
|
commitdiff
2018-03-09
Mathias Preiner
Fix Travis for unit test compilation errors. (#1651)
tree
|
commitdiff
2018-03-06
Andres Noetzli
Remove printf from output utilities (#1629)
tree
|
commitdiff
2018-03-06
Andrew Reynolds
Update semantics for string indexof and replace (#1630)
tree
|
commitdiff
2018-03-05
Aina Niemetz
Add support for check-sat-assuming. (#1637)
tree
|
commitdiff
2018-02-28
Andrew Reynolds
Minor fixes for rec-fun (#1616)
tree
|
commitdiff
2018-02-27
Andrew Reynolds
Improve rewriter for string indexof (#1592)
tree
|
commitdiff
2018-02-24
Andres Noetzli
Add unit tests for BitVector, minor BV rewrite fix...
tree
|
commitdiff
2018-02-23
Andrew Reynolds
Fix cd-simplification for strings (#1624)
tree
|
commitdiff
2018-02-22
Andrew Reynolds
Minor improvements to string rewriter (#1572)
tree
|
commitdiff
2018-02-20
Andrew Reynolds
Minor fixes and additions for transcendental functions...
tree
|
commitdiff
2018-02-16
Aina Niemetz
Make regress1 default, only test regress0 on Travis...
tree
|
commitdiff
2018-02-15
Andrew Reynolds
Fix corner case for rewrite of mult by pow 2 (#1601)
tree
|
commitdiff
2018-02-15
Andrew Reynolds
Refactor regressions (#1581)
tree
|
commitdiff
2018-02-15
Andres Noetzli
Fix context memory manager unit test (#1609)
tree
|
commitdiff
2018-02-14
Andrew Reynolds
Quantifiers subdirectories (#1608)
tree
|
commitdiff
2018-02-09
Tim King
Renaming CHECK to CVC4_CHECK. This avoids name collisio...
tree
|
commitdiff
2018-02-08
Aina Niemetz
Updated copyright
tree
|
commitdiff
2018-02-08
Andres Noetzli
Remove invalid regression test (#1579)
tree
|
commitdiff
2018-02-07
Tim King
Adds a new CHECK macro that abort()s on failure. (...
tree
|
commitdiff
2018-02-07
Andrew Reynolds
Add remaining transcendental functions (#1551)
tree
|
commitdiff
2018-02-06
Andrew Reynolds
Fix two multiply-by-constant corner cases for bv rewrit...
tree
|
commitdiff
2018-02-06
Andrew Reynolds
Fix rewrite for string replace (#1537)
tree
|
commitdiff
2018-02-06
Andrew Reynolds
Statically eliminate redundant sygus constructors ...
tree
|
commitdiff
2018-02-02
Andrew Reynolds
Fix remaining synthesis solution regressions (#1557)
tree
|
commitdiff
2018-02-02
Haniel Barbosa
Option to check solutions produced by SyGuS solver...
tree
|
commitdiff
2018-01-25
Aina Niemetz
Added unit tests for PLUS, NEG, NOT ICs for CBQI BV...
tree
|
commitdiff
2018-01-22
Aina Niemetz
Refactor and fix solveBvLit for CBQI BV. (#1526)
tree
|
commitdiff
2018-01-12
Andrew Reynolds
Improvements for CBQI BV (#1504)
tree
|
commitdiff
2018-01-10
Mathias Preiner
Fix linearization for terms where the solve variable...
tree
|
commitdiff
2018-01-08
Andrew Reynolds
Improvements to quant+BV/Bool variable elimination...
tree
|
commitdiff
2018-01-05
Mathias Preiner
Add UGT/SGT side conditions for AND/OR + other fixes...
tree
|
commitdiff
2018-01-03
Andrew Reynolds
Global negate (#1466)
tree
|
commitdiff
2018-01-03
Aina Niemetz
Add side conditions for inequalities over BITVECTOR_UDI...
tree
|
commitdiff
2018-01-03
Mathias Preiner
Fix handling for UGT/SGT. (#1467)
tree
|
commitdiff
2018-01-02
Andrew Reynolds
Rewrites for BitVector multiplication (#1465)
tree
|
commitdiff
2017-12-30
Aina Niemetz
Add side conditions for inequalities over BITVECTOR_URE...
tree
|
commitdiff
2017-12-29
Aina Niemetz
Fix unit tests for ineq for CBQI BV. (#1456)
tree
|
commitdiff
2017-12-29
Aina Niemetz
Add unit tests for side conditions for inequality for...
tree
|
commitdiff
2017-12-28
Arjun Viswanathan
Rel smt parser (#1446)
tree
|
commitdiff
2017-12-21
Andrew Reynolds
Fixes for cbqi-bv (#1449)
tree
|
commitdiff
2017-12-21
Aina Niemetz
Add explicit disequality handling when generating side...
tree
|
commitdiff
2017-12-20
Andrew Reynolds
Transcendental functions check model (#1443)
tree
|
commitdiff
2017-12-14
Aina Niemetz
Add missing side conditions for SHL, LSHR, ASHR for...
tree
|
commitdiff
next