projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Replace deprecated calls to `std::allocator` (#6606)
2021-05-24
Andrew Reynolds
Fix non-fixed length case in re-elim (#6612)
commit
|
commitdiff
|
tree
2021-05-24
Andrew Reynolds
Implementation of the new justification heuristic ...
commit
|
commitdiff
|
tree
2021-05-24
Andrew Reynolds
Move proof utilities to src/proof/ (#6611)
commit
|
commitdiff
|
tree
2021-05-24
Andrew Reynolds
Fix re-elim length requirement for symbolic RE memberships...
commit
|
commitdiff
|
tree
2021-05-24
Andrew Reynolds
Fix instance of no rewrite in extended rewriter (#6610)
commit
|
commitdiff
|
tree
2021-05-24
Andrew Reynolds
Better formalization of regular expression unfolding...
commit
|
commitdiff
|
tree
2021-05-21
Andrew Reynolds
Fix tests of unsat cores (#6593)
commit
|
commitdiff
|
tree
2021-05-21
Andrew Reynolds
Fix and refactor relevant domain (#6528)
commit
|
commitdiff
|
tree
2021-05-21
Andrew Reynolds
Formalize shared selectors as skolem functions (#6591)
commit
|
commitdiff
|
tree
2021-05-21
Andrew Reynolds
Minor simplification to boolean proof checker (#6590)
commit
|
commitdiff
|
tree
2021-05-21
Andrew Reynolds
(proof-new) Minor documentation sync (#6592)
commit
|
commitdiff
|
tree
2021-05-21
Andrew Reynolds
Add utility to get all types occurring in a term (...
commit
|
commitdiff
|
tree
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
next