projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first
⋅
prev
⋅
next
Integrate installation instructions into documentation (#6814)
2021-05-21
Andrew Reynolds
Update to sygus standard output for check-synth responses...
commit
|
commitdiff
|
tree
2021-05-19
Andrew Reynolds
Pass empty vector when constructing re empty, fixes...
commit
|
commitdiff
|
tree
2021-05-19
Andrew Reynolds
Make strings emp inference an unhandled inference for...
commit
|
commitdiff
|
tree
2021-05-19
Andrew Reynolds
Fix strings rewriter for non-standard re range (#6570)
commit
|
commitdiff
|
tree
2021-05-19
Andrew Reynolds
Add more missing inference ids (#6313)
commit
|
commitdiff
|
tree
2021-05-19
Andrew Reynolds
Fix positive contains indexof rewrites for empty string...
commit
|
commitdiff
|
tree
2021-05-19
Andrew Reynolds
Fix handling of non-standard re.range terms (#6563)
commit
|
commitdiff
|
tree
2021-05-18
Andrew Reynolds
(proof-new) Miscellaneous updates to strings from proof...
commit
|
commitdiff
|
tree
2021-05-18
Andrew Reynolds
Fix smt2 printing (#6558)
commit
|
commitdiff
|
tree
2021-05-12
Andrew Reynolds
Preliminary draft of changes for SMT comp 2021 (#6522)
commit
|
commitdiff
|
tree
2021-05-12
Andrew Reynolds
Ensure sequences of Booleans generate Boolean term...
commit
|
commitdiff
|
tree
2021-05-10
Andrew Reynolds
Unify top-level substitutions and model substitutions...
commit
|
commitdiff
|
tree
2021-05-08
Andrew Reynolds
Add support for datatype update (#6449)
commit
|
commitdiff
|
tree
2021-05-07
Andrew Reynolds
Simplifications to expand definitions (#6487)
commit
|
commitdiff
|
tree
2021-05-06
Andrew Reynolds
Discard duplicate terms in patterns (#6501)
commit
|
commitdiff
|
tree
2021-05-06
Andrew Reynolds
Use constant folding for evaluating BV eager atom ...
commit
|
commitdiff
|
tree
2021-05-05
Andrew Reynolds
Do not have quantifiers model inherit from theory model...
commit
|
commitdiff
|
tree
2021-05-05
Andrew Reynolds
Move current decision engine to decision engine old...
commit
|
commitdiff
|
tree
2021-05-04
Andrew Reynolds
Move env into smt solver, theory engine, prop engine...
commit
|
commitdiff
|
tree
2021-04-30
Andrew Reynolds
Use substitutions for implementing defined functions...
commit
|
commitdiff
|
tree
2021-04-29
Andrew Reynolds
Add assertion list utility for justification heuristic...
commit
|
commitdiff
|
tree
2021-04-27
Andrew Reynolds
Add internal support for datatype update (#6450)
commit
|
commitdiff
|
tree
2021-04-27
Andrew Reynolds
Move slow regression to regress3 (#6451)
commit
|
commitdiff
|
tree
2021-04-27
Andrew Reynolds
Fix refutational soundness bug in quantifier prenexing...
commit
|
commitdiff
|
tree
2021-04-27
Andrew Reynolds
Simplify making function types (#6447)
commit
|
commitdiff
|
tree
2021-04-26
Andrew Reynolds
Fix theoryOf for Boolean equalities (#6444)
commit
|
commitdiff
|
tree
2021-04-26
Andrew Reynolds
Ensure dependency is tracked for all substitutions...
commit
|
commitdiff
|
tree
2021-04-26
Andrew Reynolds
Enable print-inst-full by default (#6435)
commit
|
commitdiff
|
tree
2021-04-26
Andrew Reynolds
Do not process looping word equations over sequences...
commit
|
commitdiff
|
tree
2021-04-25
Andrew Reynolds
Use fast enumeration by default for Boolean predicate...
commit
|
commitdiff
|
tree
2021-04-25
Andrew Reynolds
More check models (#6439)
commit
|
commitdiff
|
tree
2021-04-24
Andrew Reynolds
Improve getValue for non-evaluated operators (#6436)
commit
|
commitdiff
|
tree
2021-04-23
Andrew Reynolds
(proof-new) Proofs for sets purification lemmas (#6416)
commit
|
commitdiff
|
tree
2021-04-23
Andrew Reynolds
Add new substitution apply methods fixpoint, sequential...
commit
|
commitdiff
|
tree
2021-04-23
Andrew Reynolds
Enable strings exp by default for strings specific...
commit
|
commitdiff
|
tree
2021-04-23
Andrew Reynolds
Move implementation of UF rewriter to cpp (#6393)
commit
|
commitdiff
|
tree
2021-04-22
Andrew Reynolds
Make trust substitution map generate proofs lazily...
commit
|
commitdiff
|
tree
2021-04-22
Andrew Reynolds
Minor improvements to substitutions (#6380)
commit
|
commitdiff
|
tree
2021-04-22
Andrew Reynolds
Minor changes to unsat core default setting (#6425)
commit
|
commitdiff
|
tree
2021-04-22
Andrew Reynolds
Reorganizing use of skolem definition manager in prop...
commit
|
commitdiff
|
tree
2021-04-22
Andrew Reynolds
Fix models for sygus-inference, bv2int, real2int (...
commit
|
commitdiff
|
tree
2021-04-22
Andrew Reynolds
Move expand definition from Theory to TheoryRewriter...
commit
|
commitdiff
|
tree
2021-04-21
Andrew Reynolds
Add unit test for abduction (#6400)
commit
|
commitdiff
|
tree
2021-04-21
Andrew Reynolds
Add basic utilities for new implementation of justification...
commit
|
commitdiff
|
tree
2021-04-20
Andrew Reynolds
Split FP expand definitions to own module (#6392)
commit
|
commitdiff
|
tree
2021-04-20
Andrew Reynolds
Add instantiation pool feature to the API (#6358)
commit
|
commitdiff
|
tree
2021-04-19
Andrew Reynolds
Fully incorporate quantifiers macros into ppAssert...
commit
|
commitdiff
|
tree
2021-04-16
Andrew Reynolds
Fix ONCE for post-rewrite (#6372)
commit
|
commitdiff
|
tree
2021-04-15
Andrew Reynolds
Reenable regression for minimizing instantiations ...
commit
|
commitdiff
|
tree
2021-04-14
Andrew Reynolds
Fix type rule for relations join image (#6349)
commit
|
commitdiff
|
tree
2021-04-14
Andrew Reynolds
Add internal API methods for pool-based instantiation...
commit
|
commitdiff
|
tree
2021-04-14
Andrew Reynolds
Add interface for getting relevant assertions (#5131)
commit
|
commitdiff
|
tree
2021-04-14
Andrew Reynolds
Warn about infeasible SyGuS conjectures (#6345)
commit
|
commitdiff
|
tree
2021-04-13
Andrew Reynolds
Add pool instantiation strategy (#6308)
commit
|
commitdiff
|
tree
2021-04-13
Andrew Reynolds
Refactor quantifiers macros (#6348)
commit
|
commitdiff
|
tree
2021-04-13
Andrew Reynolds
Formalize more skolems (#6307)
commit
|
commitdiff
|
tree
2021-04-12
Andrew Reynolds
Fix computation of whether a type is finite (#6312)
commit
|
commitdiff
|
tree
2021-04-12
Andrew Reynolds
Consolidate interface to prop engine (#6189)
commit
|
commitdiff
|
tree
2021-04-09
Andrew Reynolds
Add identifiers for extended function reductions (...
commit
|
commitdiff
|
tree
2021-04-09
Andrew Reynolds
Add regressions for issue 6214 (#6305)
commit
|
commitdiff
|
tree
2021-04-09
Andrew Reynolds
Avoid spurious runs in run_regression.py (#6318)
commit
|
commitdiff
|
tree
2021-04-09
Andrew Reynolds
Use expr miner timeout (#6321)
commit
|
commitdiff
|
tree
2021-04-08
Andrew Reynolds
Fix run_regression for cvc expected outputs (#6317)
commit
|
commitdiff
|
tree
2021-04-08
Andrew Reynolds
Use exceptions when constructing malformed datatypes...
commit
|
commitdiff
|
tree
2021-04-08
Andrew Reynolds
Add identifiers for sources of incompleteness (#6311)
commit
|
commitdiff
|
tree
2021-04-08
Andrew Reynolds
Add benchmark for issue 5101 (#6301)
commit
|
commitdiff
|
tree
2021-04-08
Andrew Reynolds
Add benchmark for issue 4400 (#6288)
commit
|
commitdiff
|
tree
2021-04-08
Andrew Reynolds
Initial support for parametric datatypes in sygus ...
commit
|
commitdiff
|
tree
2021-04-07
Andrew Reynolds
Add cardinality class definition (#6302)
commit
|
commitdiff
|
tree
2021-04-07
Andrew Reynolds
Add benchmark for 6270 (#6283)
commit
|
commitdiff
|
tree
2021-04-07
Andrew Reynolds
Add benchmark for issue 4420 (#6286)
commit
|
commitdiff
|
tree
2021-04-07
Andrew Reynolds
Set incomplete if not applying ho extensionality (...
commit
|
commitdiff
|
tree
2021-04-07
Andrew Reynolds
Fixes for abducts (#6279)
commit
|
commitdiff
|
tree
2021-04-07
Andrew Reynolds
(proof-new) Proper implementation of proof node cloning...
commit
|
commitdiff
|
tree
2021-04-07
Andrew Reynolds
Add term pools utility (#6243)
commit
|
commitdiff
|
tree
2021-04-07
Andrew Reynolds
Replace calls to NodeManager::mkSkolem with SkolemManager...
commit
|
commitdiff
|
tree
2021-04-06
Andrew Reynolds
Add benchmark for issue 5942 (#6296)
commit
|
commitdiff
|
tree
2021-04-06
Andrew Reynolds
Fix tptp parser for negative rational (#6297)
commit
|
commitdiff
|
tree
2021-04-06
Andrew Reynolds
Fix issue with lemma during equality engine iterator...
commit
|
commitdiff
|
tree
2021-04-06
Andrew Reynolds
Remove stdPrintAscii option (#6280)
commit
|
commitdiff
|
tree
2021-04-05
Andrew Reynolds
Fix spurious antecedant for symbolic regular expressions...
commit
|
commitdiff
|
tree
2021-04-05
Andrew Reynolds
Add benchmark for issue 4412 (#6287)
commit
|
commitdiff
|
tree
2021-04-05
Andrew Reynolds
Enable UF when pre-skolem nested option is enabled...
commit
|
commitdiff
|
tree
2021-04-05
Andrew Reynolds
Fix subtyping for sets care graph (#6278)
commit
|
commitdiff
|
tree
2021-04-05
Andrew Reynolds
Add interface for skolem functions in SkolemManager...
commit
|
commitdiff
|
tree
2021-04-03
Andrew Reynolds
Disable substring component contains in strip endpoints...
commit
|
commitdiff
|
tree
2021-04-02
Andrew Reynolds
Cleaning up friend relationships for commands (#6254)
commit
|
commitdiff
|
tree
2021-04-02
Andrew Reynolds
Fix case where RE unfolding generates a trivially true...
commit
|
commitdiff
|
tree
2021-04-01
Andrew Reynolds
Simplify caching of regular expression unfolding (...
commit
|
commitdiff
|
tree
2021-04-01
Andrew Reynolds
Fix type rule for to_real (#6257)
commit
|
commitdiff
|
tree
2021-04-01
Andrew Reynolds
Add regression for issue 6191 (#6264)
commit
|
commitdiff
|
tree
2021-04-01
Andrew Reynolds
Add debug traces to theory inference manager (#6250)
commit
|
commitdiff
|
tree
2021-04-01
Andrew Reynolds
Fix non-linear for unknown case (#6252)
commit
|
commitdiff
|
tree
2021-03-31
Andrew Reynolds
Eliminate dependencies on quantifiers engine in internal...
commit
|
commitdiff
|
tree
2021-03-31
Andrew Reynolds
Add missing inference ids (#6242)
commit
|
commitdiff
|
tree
2021-03-30
Andrew Reynolds
Fix printing for double patterns (#6235)
commit
|
commitdiff
|
tree
2021-03-30
Andrew Reynolds
Make SEXPR simply typed (#6160)
commit
|
commitdiff
|
tree
2021-03-30
Andrew Reynolds
Implement simple tracking of instantiation lemmas ...
commit
|
commitdiff
|
tree
2021-03-30
Andrew Reynolds
Refactoring quantifier annotation kinds, add kinds...
commit
|
commitdiff
|
tree
2021-03-30
Andrew Reynolds
Eliminate use of rational from tptp parser (#6239)
commit
|
commitdiff
|
tree
next