projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cmake: Working build infrastructure.
[cvc5.git]
/
test
/
2018-09-22
Aina Niemetz
cmake: Added initial build infrastructure.
tree
|
commitdiff
2018-09-19
Andres Noetzli
Add rewrites for str.contains + str.replace/substr...
tree
|
commitdiff
2018-09-18
Andres Noetzli
Fix issue with str.idof in evaluator (#2493)
tree
|
commitdiff
2018-09-18
Andrew Reynolds
Improvements and fixes for symmetry detection and break...
tree
|
commitdiff
2018-09-17
Andrew Reynolds
Make strings model construction robust to lengths that...
tree
|
commitdiff
2018-09-15
Andres Noetzli
Refactor how assertions are added to decision engine...
tree
|
commitdiff
2018-09-14
Andrew Reynolds
Generalize CandidateRewriteDatabase to ExprMiner (...
tree
|
commitdiff
2018-09-13
Haniel Barbosa
Uses information gain heuristic for building better...
tree
|
commitdiff
2018-09-11
Andrew Reynolds
Support model cores via option --produce-model-cores...
tree
|
commitdiff
2018-09-11
Andrew Reynolds
Fix global negate (#2449)
tree
|
commitdiff
2018-09-10
Andres Noetzli
Add (str.replace (str.replace y w y) y z) rewrite ...
tree
|
commitdiff
2018-09-06
Andrew Reynolds
Refactor and document quantifiers variable elimination...
tree
|
commitdiff
2018-09-05
Andres Noetzli
Add regex grammar to rewriter verification tests (...
tree
|
commitdiff
2018-09-05
Andrew Reynolds
Extended rewriter for string equalities (#2427)
tree
|
commitdiff
2018-09-04
Andres Noetzli
Remove CVC3 compatibility layer (#2418)
tree
|
commitdiff
2018-09-04
Andrew Reynolds
Make quantifiers strategies exit immediately when in...
tree
|
commitdiff
2018-08-30
Andrew Reynolds
Add regular expression elimination module (#2400)
tree
|
commitdiff
2018-08-28
Andrew Reynolds
Fix for get constraints method in fmf-fun (#2399)
tree
|
commitdiff
2018-08-28
Andrew Reynolds
Fix sort inference for quantified variables of interpre...
tree
|
commitdiff
2018-08-28
Andrew Reynolds
Refactor extended rewriter, move rewrites to aggressive...
tree
|
commitdiff
2018-08-27
Andrew Reynolds
Make division chainable in the smt2 parser (#2367)
tree
|
commitdiff
2018-08-25
Haniel Barbosa
Refactor nlExtPurify preprocessing pass (#1963)
tree
|
commitdiff
2018-08-24
Andrew Reynolds
Remove spurious disabling of cbqi-all (#2368)
tree
|
commitdiff
2018-08-24
Andres Noetzli
Add tests that enumerate and verify rewrite rules ...
tree
|
commitdiff
2018-08-23
Andres Noetzli
Add missing overrides in unit tests (#2362)
tree
|
commitdiff
2018-08-23
Andrew Reynolds
Fix regression requiring proof build. (#2364)
tree
|
commitdiff
2018-08-23
Andrew Reynolds
More regressions that increase coverage (#2354)
tree
|
commitdiff
2018-08-22
yoni206
Generating less consistency lemmas in bv-ackermann...
tree
|
commitdiff
2018-08-22
Andrew Reynolds
Fix option for real2int regression. (#2353)
tree
|
commitdiff
2018-08-22
Haniel Barbosa
Adds regression test for automatic generation of SyGuS...
tree
|
commitdiff
2018-08-22
Andrew Reynolds
Fix processing of nested Variable construct in sygus...
tree
|
commitdiff
2018-08-21
Haniel Barbosa
Makes the new row propagation system default (#2335)
tree
|
commitdiff
2018-08-21
Andrew Reynolds
Use cbqi-full for sygus (#2346)
tree
|
commitdiff
2018-08-21
Andres Noetzli
Remove support for *.expect files in regressions (...
tree
|
commitdiff
2018-08-21
Aina Niemetz
Remove disabled system test cvc3_george. (#2342)
tree
|
commitdiff
2018-08-20
Andrew Reynolds
Add regressions that increase coverage (#2337)
tree
|
commitdiff
2018-08-18
Aina Niemetz
run-regress script: Exit with exit code > 0 on failure...
tree
|
commitdiff
2018-08-17
Andrew Reynolds
Remove support for flipDecision (#2319)
tree
|
commitdiff
2018-08-17
Andrew Reynolds
Add sygus stream regressions (#2330)
tree
|
commitdiff
2018-08-17
Andrew Reynolds
Fix spurious warning in sort inference (#2331)
tree
|
commitdiff
2018-08-17
Andrew Reynolds
Eliminate partial operators in sygus grammar normaliza...
tree
|
commitdiff
2018-08-16
Haniel Barbosa
Refactor extended rewriter preprocessing pass (#2324)
tree
|
commitdiff
2018-08-16
Haniel Barbosa
Refactor apply2const (#2316)
tree
|
commitdiff
2018-08-15
Andrew Reynolds
Make sort inference a preprocessing pass (#2309)
tree
|
commitdiff
2018-08-14
Andres Noetzli
Fix get-unsat-assumptions output (#2301)
tree
|
commitdiff
2018-08-13
Tim King
Removing support for T* and const T* attributes. (...
tree
|
commitdiff
2018-08-10
Andres Noetzli
Do not use static initialization in CxxTest runner...
tree
|
commitdiff
2018-08-09
Andrew Reynolds
Fix char overflow issues in regular expression solver...
tree
|
commitdiff
2018-08-09
Andres Noetzli
Fix documentation of regression tests (#2290)
tree
|
commitdiff
2018-08-09
Aina Niemetz
Plug solver API object into parser. (#2240)
tree
|
commitdiff
2018-08-08
Tim King
Proposal for adding map utility functions to CVC4...
tree
|
commitdiff
2018-08-08
Andrew Reynolds
Disable argument relevance for sygus by default (#2288)
tree
|
commitdiff
2018-08-08
Andrew Reynolds
Fix simple reg exp consume rewrite (#2281)
tree
|
commitdiff
2018-08-07
Andrew Reynolds
Fix inference of pre and post conditions for non variab...
tree
|
commitdiff
2018-08-07
Andrew Reynolds
Add RegLan to smt2/sygus parsers. (#2276)
tree
|
commitdiff
2018-08-07
Andrew Reynolds
Remove support for Enum sygus syntax. (#2264)
tree
|
commitdiff
2018-08-06
Andrew Reynolds
Fixes and improvements for single invocation inference...
tree
|
commitdiff
2018-08-06
Andrew Reynolds
Fix degenerate case of sygus grammar construction for...
tree
|
commitdiff
2018-08-02
Andrew Reynolds
Parse standard separation logic inputs (#2257)
tree
|
commitdiff
2018-08-02
Andrew Reynolds
Improve CEGQI heuristics involving equality and multipl...
tree
|
commitdiff
2018-08-02
Andrew Reynolds
Improvements and fixes in cegqi arithmetic (#2247)
tree
|
commitdiff
2018-08-01
Aina Niemetz
InteractiveShell: Remove redundant options argument...
tree
|
commitdiff
2018-08-01
Andrew Reynolds
Fix issues with bv2nat (#2219)
tree
|
commitdiff
2018-08-01
ayveejay
Improvements and tests for the API around separation...
tree
|
commitdiff
2018-07-30
Mathias Preiner
Add support for incremental eager bit-blasting. (#1838)
tree
|
commitdiff
2018-07-26
yoni206
Disabling bvLazyRewriteExtf in the right place (#2214)
tree
|
commitdiff
2018-07-26
Andrew Reynolds
Fix rewriter for lambda (#2211)
tree
|
commitdiff
2018-07-24
Andrew Reynolds
Improvements to sets + cardinality + quantifiers (...
tree
|
commitdiff
2018-07-23
Andrew Reynolds
sygusComp2018: add regressions (#2191)
tree
|
commitdiff
2018-07-21
Andrew Reynolds
Optimizations and fixes for computing whether a type...
tree
|
commitdiff
2018-07-21
yoni206
Remove --no-check-proofs and --no-check-unsat-cores...
tree
|
commitdiff
2018-07-17
yoni206
Refactor sep-pre-skolem-emp preprocessing pass
tree
|
commitdiff
2018-07-13
Andres Noetzli
Properly clean up assertion stack in CnfProof (#2147)
tree
|
commitdiff
2018-07-13
Andrew Reynolds
sygusComp2018: optimization for collect model info...
tree
|
commitdiff
2018-07-05
Andres Noetzli
sygusComp2018: Improve string rewriter (#2141)
tree
|
commitdiff
2018-07-04
Andres Noetzli
Remove unused CDVector (#2139)
tree
|
commitdiff
2018-07-03
Andres Noetzli
Add regression test for issue #1986 (#2114)
tree
|
commitdiff
2018-07-02
Aina Niemetz
Refactor ApplySubsts preprocessing pass. (#2120)
tree
|
commitdiff
2018-07-02
Andrew Reynolds
Modify cegqi heuristic for finite datatypes (#2126)
tree
|
commitdiff
2018-06-28
Andres Noetzli
Fix stale reference in MiniSat when generating UC ...
tree
|
commitdiff
2018-06-28
Andrew Reynolds
Split and document ceg theory instantiators (#2094)
tree
|
commitdiff
2018-06-26
Andres Noetzli
sygusComp2018: Add evaluator (#2090)
tree
|
commitdiff
2018-06-25
Aina Niemetz
Updated copyright headers.
tree
|
commitdiff
2018-06-21
Andres Noetzli
Check unsat cores in regressions also without LFSC...
tree
|
commitdiff
2018-06-15
Andrew Reynolds
Disable solving non-linear BV literals by default ...
tree
|
commitdiff
2018-06-13
Andrew Reynolds
Fix simple regexp consume (#2066)
tree
|
commitdiff
2018-06-12
Andrew Reynolds
Fix strip constant endpoint for ITOS in strings rewrite...
tree
|
commitdiff
2018-06-11
Andrew Reynolds
Fix equality conflicts reported by FP (#2064)
tree
|
commitdiff
2018-06-10
Andres Noetzli
Disable test that fails in competition mode (#2063)
tree
|
commitdiff
2018-06-09
Andres Noetzli
Add flag to skip regression if feature enabled (#2062)
tree
|
commitdiff
2018-06-09
Andres Noetzli
Reset decisions at SAT level after solving (#2059)
tree
|
commitdiff
2018-06-05
Andres Noetzli
Only enable transcendentals if logic is N[I]RAT (#2052)
tree
|
commitdiff
2018-06-04
Andrew Reynolds
Enable cegqi (with model values) for floating point...
tree
|
commitdiff
2018-06-04
Andres Noetzli
Regressions: Support for requiring CVC4 features (...
tree
|
commitdiff
2018-06-02
Mathias Preiner
Fix BV-abstraction check to consider SKOLEM. (#2042)
tree
|
commitdiff
2018-06-02
Andrew Reynolds
Fix preinitialization pass for finite model finding...
tree
|
commitdiff
2018-06-01
Andrew Reynolds
Fix quantified bv variable elimination (#2039)
tree
|
commitdiff
2018-06-01
Andrew Reynolds
Apply preprocessing to counterexample lemmas in CEGQI...
tree
|
commitdiff
2018-06-01
Andrew Reynolds
Use monomial sum utility to solve for quantifiers...
tree
|
commitdiff
2018-05-31
Mathias Preiner
Fix bv-abstraction check for AND with non bit-vector...
tree
|
commitdiff
next