projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Generalize interface for candidate rewrite database (#4797)
2020-08-03
Andrew Reynolds
Generalize interface for candidate rewrite database...
commit
|
commitdiff
|
tree
2020-08-03
Andrew Reynolds
Update datatypes in cvc parser to the new API (#4826)
commit
|
commitdiff
|
tree
2020-08-03
Andrew Reynolds
Split expression names from SmtEngine (#4832)
commit
|
commitdiff
|
tree
2020-08-03
Andrew Reynolds
Split dump manager from SmtEngine (#4824)
commit
|
commitdiff
|
tree
2020-08-02
Andrew Reynolds
Updates to dtype constructor in preparation for eliminating...
commit
|
commitdiff
|
tree
2020-08-02
Andrew Reynolds
Add methods for constructing datatype types from NodeManager...
commit
|
commitdiff
|
tree
2020-08-01
Andrew Reynolds
Fix component contains for splicing due to substring...
commit
|
commitdiff
|
tree
2020-07-31
Andrew Reynolds
Split listener classes from SmtEngine (#4816)
commit
|
commitdiff
|
tree
2020-07-31
Andrew Reynolds
Standardize explanations in arrays (#4804)
commit
|
commitdiff
|
tree
2020-07-30
Andrew Reynolds
Fix null case for sygus printing (#4793)
commit
|
commitdiff
|
tree
2020-07-30
Andrew Reynolds
(proof-new) Stream output for ProofNode (#4789)
commit
|
commitdiff
|
tree
2020-07-30
Andrew Reynolds
(proof-new) Fixes for getFreeAssumptions (#4802)
commit
|
commitdiff
|
tree
2020-07-28
Andrew Reynolds
Remove arrays lazy rintro option (#4806)
commit
|
commitdiff
|
tree
2020-07-28
Andrew Reynolds
Fix regular expression delta for complement (#4765)
commit
|
commitdiff
|
tree
2020-07-28
Andrew Reynolds
Use lemma property enum for OutputChannel::lemma (...
commit
|
commitdiff
|
tree
2020-07-27
Andrew Reynolds
(proof-new) Proof production for term formula removal...
commit
|
commitdiff
|
tree
2020-07-27
Andrew Reynolds
(proof-new) Arithmetic operator elim proof producing...
commit
|
commitdiff
|
tree
2020-07-21
Andrew Reynolds
Support uninterpreted constants in the evaluator (...
commit
|
commitdiff
|
tree
2020-07-18
Andrew Reynolds
(proof-new) Proof recording for assertions pipeline...
commit
|
commitdiff
|
tree
2020-07-18
Andrew Reynolds
Enumerate shapes feature in fast sygus enumerator ...
commit
|
commitdiff
|
tree
2020-07-17
Andrew Reynolds
Replace options listener infrastructure (#4764)
commit
|
commitdiff
|
tree
2020-07-17
Andrew Reynolds
(proof-new) Updates to strings core solver (#4642)
commit
|
commitdiff
|
tree
2020-07-17
Andrew Reynolds
Add option manager and simpler option listener (#4745)
commit
|
commitdiff
|
tree
2020-07-16
Andrew Reynolds
Split abstract values utility from SmtEngine (#4754)
commit
|
commitdiff
|
tree
2020-07-16
Andrew Reynolds
Make ExtTheory a utility and not a member of Theory...
commit
|
commitdiff
|
tree
2020-07-15
Andrew Reynolds
Split abduction solver from SmtEngine (#4733)
commit
|
commitdiff
|
tree
2020-07-15
Andrew Reynolds
Simplify entailment check interface (#4744)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Make use of options in setDefaults more consistent...
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Remove sygus print callback (#4727)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Fix regression output. (#4741)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
(proof-new) Skeleton proof support in the Rewriter...
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Debug instantiations output (#4739)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Minor refactoring of subsolver initialization (#4731)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Fix type comparisons involving pointer. (#4738)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Fix whitespace issue in instantiations output. (#4737)
commit
|
commitdiff
|
tree
2020-07-13
Andrew Reynolds
(proof-new) SMT Preprocess proof generator (#4708)
commit
|
commitdiff
|
tree
2020-07-13
Andrew Reynolds
User-facing print debug option for sygus candidates...
commit
|
commitdiff
|
tree
2020-07-13
Andrew Reynolds
Statistics on instantiations per quantified formula...
commit
|
commitdiff
|
tree
2020-07-13
Andrew Reynolds
Add support for string/sequence update (#4725)
commit
|
commitdiff
|
tree
2020-07-11
Andrew Reynolds
Cache explanations in TheoryEngine::getExplanation...
commit
|
commitdiff
|
tree
2020-07-11
Andrew Reynolds
(proof-new) Add ONCE and FIXPOINT modes for term conversion...
commit
|
commitdiff
|
tree
2020-07-11
Andrew Reynolds
(proof-new) Update Theory interface for proof-new ...
commit
|
commitdiff
|
tree
2020-07-10
Andrew Reynolds
Front end support for integer AND (#4717)
commit
|
commitdiff
|
tree
2020-07-10
Andrew Reynolds
Update competition scripts (#4715)
commit
|
commitdiff
|
tree
2020-07-10
Andrew Reynolds
Ensure legal elimination for witness rewrite (#4688)
commit
|
commitdiff
|
tree
2020-07-09
Andrew Reynolds
Disable unsat cores in timeout regression (#4713)
commit
|
commitdiff
|
tree
2020-07-09
Andrew Reynolds
Associate all lemmas in non-linear arithmetic with...
commit
|
commitdiff
|
tree
2020-07-09
Andrew Reynolds
(proof-new) Theory engine proof generator (#4657)
commit
|
commitdiff
|
tree
2020-07-08
Andrew Reynolds
Always interleave theory combination with quantifiers...
commit
|
commitdiff
|
tree
2020-07-08
Andrew Reynolds
Improve and fix secant and tangent lemmas in the transcenden...
commit
|
commitdiff
|
tree
2020-07-07
Andrew Reynolds
Transfer ownership of internal Options from NodeManager...
commit
|
commitdiff
|
tree
2020-07-06
Andrew Reynolds
Front end support for sequences (#4690)
commit
|
commitdiff
|
tree
2020-07-02
Andrew Reynolds
Fix regression option (#4680)
commit
|
commitdiff
|
tree
2020-07-02
Andrew Reynolds
(proof-new) Updates to skolem manager interface (...
commit
|
commitdiff
|
tree
2020-07-02
Andrew Reynolds
(proof-new) Proof rule checkers run on skolem forms...
commit
|
commitdiff
|
tree
2020-07-02
Andrew Reynolds
(proof-new) Proof node updater (#4647)
commit
|
commitdiff
|
tree
2020-07-01
Andrew Reynolds
Add solver for integer AND (#4681)
commit
|
commitdiff
|
tree
2020-07-01
Andrew Reynolds
Inferences and model construction taking into account...
commit
|
commitdiff
|
tree
2020-07-01
Andrew Reynolds
(proof-new) Updates to evaluator (#4659)
commit
|
commitdiff
|
tree
2020-07-01
Andrew Reynolds
(proof-new) Improve rewriter for WITNESS (#4661)
commit
|
commitdiff
|
tree
2020-06-30
Andrew Reynolds
Fix normal form for re.comp (#4676)
commit
|
commitdiff
|
tree
2020-06-30
Andrew Reynolds
Simplify quantifiers strategy for when to apply last...
commit
|
commitdiff
|
tree
2020-06-30
Andrew Reynolds
Add internal support for integer and operator (#4668)
commit
|
commitdiff
|
tree
2020-06-28
Andrew Reynolds
Fix non-termination issues in simpleRegExpConsume ...
commit
|
commitdiff
|
tree
2020-06-25
Andrew Reynolds
(proof-new) Add TrustNode interfaces to OutputChannel...
commit
|
commitdiff
|
tree
2020-06-25
Andrew Reynolds
Remove sygus1 parser (#4651)
commit
|
commitdiff
|
tree
2020-06-25
Andrew Reynolds
Update option --nl-ext to enable/disable incremental...
commit
|
commitdiff
|
tree
2020-06-23
Andrew Reynolds
(proof-new) Updates to proof node manager (#4617)
commit
|
commitdiff
|
tree
2020-06-22
Andrew Reynolds
(proof-new) Add REWRITE trust node kind. (#4624)
commit
|
commitdiff
|
tree
2020-06-22
Andrew Reynolds
(proof-new) Add proof-new to options file (#4641)
commit
|
commitdiff
|
tree
2020-06-22
Andrew Reynolds
Add trascendental function kinds to list of unevaluated...
commit
|
commitdiff
|
tree
2020-06-20
Andrew Reynolds
(proof-new) Make static methods in re-elim (#4623)
commit
|
commitdiff
|
tree
2020-06-19
Andrew Reynolds
(proof-new) CDProof inherits from ProofGenerator (...
commit
|
commitdiff
|
tree
2020-06-19
Andrew Reynolds
Add casc j10 scripts (#4621)
commit
|
commitdiff
|
tree
2020-06-19
Andrew Reynolds
(proof-new) Updates to strings term registry (#4599)
commit
|
commitdiff
|
tree
2020-06-19
Andrew Reynolds
Convert more uses of strings to words (#4584)
commit
|
commitdiff
|
tree
2020-06-19
Andrew Reynolds
(proof-new) Split operator elimination from arithmetic...
commit
|
commitdiff
|
tree
2020-06-19
Andrew Reynolds
Clean the header file of TheoryStrings (#4272)
commit
|
commitdiff
|
tree
2020-06-17
Andrew Reynolds
Do not traverse WITNESS for partial substitutions in...
commit
|
commitdiff
|
tree
2020-06-16
Andrew Reynolds
Updates to NEWS. (#4628)
commit
|
commitdiff
|
tree
2020-06-16
Andrew Reynolds
(proof-new) Add quantifiers proof checker (#4593)
commit
|
commitdiff
|
tree
2020-06-15
Andrew Reynolds
(proof-new) Update proof node, add proof node algorithm...
commit
|
commitdiff
|
tree
2020-06-15
Andrew Reynolds
Do RE derivation inference only for concrete constant...
commit
|
commitdiff
|
tree
2020-06-13
Andrew Reynolds
Move sygus datatype utility functions to their own...
commit
|
commitdiff
|
tree
2020-06-12
Andrew Reynolds
Update to consistent policy for removed terms in quantifier...
commit
|
commitdiff
|
tree
2020-06-12
Andrew Reynolds
(proof-new) Term conversion proof generator utility...
commit
|
commitdiff
|
tree
2020-06-12
Andrew Reynolds
(proof-new) Minor updates to strings base solver (...
commit
|
commitdiff
|
tree
2020-06-12
Andrew Reynolds
Cardinality-related inferences per type in theory of...
commit
|
commitdiff
|
tree
2020-06-12
Andrew Reynolds
(proof-new) Split TheoryEngine (#4558)
commit
|
commitdiff
|
tree
2020-06-12
Andrew Reynolds
Add rewrite for str.replace_re. (#4601)
commit
|
commitdiff
|
tree
2020-06-11
Andrew Reynolds
(proof-new) Add lazy proof utility (#4589)
commit
|
commitdiff
|
tree
2020-06-11
Andrew Reynolds
(proof-new) Add eager proof generator utility. (#4592)
commit
|
commitdiff
|
tree
2020-06-11
Andrew Reynolds
(proof-new) Remove arith-snorm option. (#4591)
commit
|
commitdiff
|
tree
2020-06-10
Andrew Reynolds
(proof-new) Theory proof step buffer utility (#4580)
commit
|
commitdiff
|
tree
2020-06-09
Andrew Reynolds
(proof-new) Refactor skolemization (#4586)
commit
|
commitdiff
|
tree
2020-06-09
Andrew Reynolds
(proof-new) Add trust node utility (#4588)
commit
|
commitdiff
|
tree
2020-06-08
Andrew Reynolds
(proof-new) Add abstract proof generator class (#4574)
commit
|
commitdiff
|
tree
2020-06-06
Andrew Reynolds
Use NlLemma utility for all lemmas in non-linear. ...
commit
|
commitdiff
|
tree
2020-06-06
Andrew Reynolds
Smt2 parsing support for nested recursive datatypes...
commit
|
commitdiff
|
tree
2020-06-05
Andrew Reynolds
Datatypes with nested recursion are not handled in...
commit
|
commitdiff
|
tree
next