projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Update option --nl-ext to enable/disable incremental linearization solver only (...
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
2020-06-05
Andrew Reynolds
(proof-new) Updates to CDProof (#4565)
commit
|
commitdiff
|
tree
2020-06-05
Andrew Reynolds
(proof-new) Rename ProofSkolemCache to SkolemManager...
commit
|
commitdiff
|
tree
2020-06-04
Andrew Reynolds
Add sygus datatype substitution utility method (#4390)
commit
|
commitdiff
|
tree
2020-06-04
Andrew Reynolds
Fix abduction with datatypes (#4566)
commit
|
commitdiff
|
tree
2020-06-04
Andrew Reynolds
Theory strings preprocess (#4534)
commit
|
commitdiff
|
tree
2020-06-03
Andrew Reynolds
(proof-new) Add builtin proof checker (#4537)
commit
|
commitdiff
|
tree
2020-06-03
Andrew Reynolds
Do not apply unconstrained simplification when quantifiers...
commit
|
commitdiff
|
tree
2020-06-03
Andrew Reynolds
Update CEGQI to use lemma status instead of forcing...
commit
|
commitdiff
|
tree
2020-06-03
Andrew Reynolds
Use prenex normal form when using cegqi-nested-qe ...
commit
|
commitdiff
|
tree
2020-06-02
Andrew Reynolds
Fix scope issue with pulling ITEs in extended rewriter...
commit
|
commitdiff
|
tree
2020-06-02
Andrew Reynolds
Do not handle universal quantification on functions...
commit
|
commitdiff
|
tree
2020-06-01
Andrew Reynolds
(proof-new) Proof step buffer utilities (#4533)
commit
|
commitdiff
|
tree
2020-06-01
Andrew Reynolds
Move non-linear files to src/theory/arith/nl (#4548)
commit
|
commitdiff
|
tree
2020-06-01
Andrew Reynolds
Incorporate sequences into the word interface (#4543)
commit
|
commitdiff
|
tree
2020-05-30
Andrew Reynolds
Add the sequence type (#4539)
commit
|
commitdiff
|
tree
2020-05-28
Andrew Reynolds
Fix term registry for constant case, simplify. (#4538)
commit
|
commitdiff
|
tree
2020-05-27
Andrew Reynolds
Add the Expr-level sequence datatype (#4526)
commit
|
commitdiff
|
tree
2020-05-26
Andrew Reynolds
Convert more uses of strings to words (#4527)
commit
|
commitdiff
|
tree
2020-05-26
Andrew Reynolds
(proof-new) Update proof checker. (#4511)
commit
|
commitdiff
|
tree
2020-05-26
Andrew Reynolds
(proof-new) Updates to strings skolem cache. (#4524)
commit
|
commitdiff
|
tree
2020-05-23
Andrew Reynolds
Add the sequence datatype (#4153)
commit
|
commitdiff
|
tree
2020-05-23
Andrew Reynolds
Refactor operator elimination in arithmetic (#4519)
commit
|
commitdiff
|
tree
2020-05-22
Andrew Reynolds
(proof-new) Add rewrite corresponding to regular expression...
commit
|
commitdiff
|
tree
2020-05-22
Andrew Reynolds
(proof-new) Proof node to SExpr utility. (#4512)
commit
|
commitdiff
|
tree
2020-05-22
Andrew Reynolds
Update string kind names in new API (#4509)
commit
|
commitdiff
|
tree
2020-05-22
Andrew Reynolds
(proof-new) Minor update to strings solver state (...
commit
|
commitdiff
|
tree
2020-05-21
Andrew Reynolds
Disable re-elim by default (#4508)
commit
|
commitdiff
|
tree
2020-05-21
Andrew Reynolds
Throw logic exception for equality between regular...
commit
|
commitdiff
|
tree
2020-05-21
Andrew Reynolds
Fix missing check for cardinality one in unconstrained...
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Normal form equality conflicts and uniqueness check...
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Add proof skolem cache (#4485)
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Fix parametric datatype instantiation (#4493)
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Use debug-check-model to enable internal debugging...
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Do not eliminate variables that are equal to unevaluatable...
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Fix cached free variable identifiers in sygus term...
commit
|
commitdiff
|
tree
2020-05-19
Andrew Reynolds
Use fresh variables when miniscoping (#4296)
commit
|
commitdiff
|
tree
2020-05-19
Andrew Reynolds
Update enum and option names for sygus languages (...
commit
|
commitdiff
|
tree
2020-05-12
Andrew Reynolds
Do not enable unconstrained simplification if arithmetic...
commit
|
commitdiff
|
tree
2020-05-05
Andrew Reynolds
Always introduce fresh variable for unconstrained APPLY_UF...
commit
|
commitdiff
|
tree
2020-05-02
Andrew Reynolds
Move slow regression to regress3 (#4430)
commit
|
commitdiff
|
tree
2020-05-01
Andrew Reynolds
Fix regression (#4424)
commit
|
commitdiff
|
tree
2020-04-30
Andrew Reynolds
Remove skolem share involving pre_first_ctn. (#4423)
commit
|
commitdiff
|
tree
2020-04-30
Andrew Reynolds
Do not mark congruent terms are reduced (#4419)
commit
|
commitdiff
|
tree
2020-04-29
Andrew Reynolds
Avoid circular dependencies for justifying reductions...
commit
|
commitdiff
|
tree
2020-04-29
Andrew Reynolds
Fix strings 2.6 regression (#4413)
commit
|
commitdiff
|
tree
2020-04-28
Andrew Reynolds
Updates to SMT COMP script for 20 minute timeout (...
commit
|
commitdiff
|
tree
2020-04-28
Andrew Reynolds
Support the SMT-LIB Unicode string standard by default...
commit
|
commitdiff
|
tree
2020-04-28
Andrew Reynolds
Update cardinality in strings to unicode standard ...
commit
|
commitdiff
|
tree
2020-04-27
Andrew Reynolds
Fix sygus unit (#4371)
commit
|
commitdiff
|
tree
2020-04-26
Andrew Reynolds
Fix sets cardinality cycle rule (#4392)
commit
|
commitdiff
|
tree
2020-04-22
Andrew Reynolds
Ensure disequality splits are processed as lemmas ...
commit
|
commitdiff
|
tree
2020-04-22
Andrew Reynolds
Allow eager bitblasting with solve bv as int in QF_NIA...
commit
|
commitdiff
|
tree
2020-04-21
Andrew Reynolds
Update to sygus version 2 (#4372)
commit
|
commitdiff
|
tree
2020-04-21
Andrew Reynolds
Fix for parse options related to binary name (#4368)
commit
|
commitdiff
|
tree
2020-04-21
Andrew Reynolds
Make option names related to CEGQI consistent (#4316)
commit
|
commitdiff
|
tree
2020-04-20
Andrew Reynolds
Refactor inference manager in strings to be amenable...
commit
|
commitdiff
|
tree
2020-04-20
Andrew Reynolds
Add SCOPE proof rule (#4332)
commit
|
commitdiff
|
tree
2020-04-19
Andrew Reynolds
Disable unsat cores on nec regression (#4330)
commit
|
commitdiff
|
tree
2020-04-18
Andrew Reynolds
Track inference id for pending facts in strings (#4331)
commit
|
commitdiff
|
tree
2020-04-17
Andrew Reynolds
Add (context-dependent) Proof (#4323)
commit
|
commitdiff
|
tree
2020-04-16
Andrew Reynolds
Add ProofNodeManager and ProofChecker (#4317)
commit
|
commitdiff
|
tree
2020-04-16
Andrew Reynolds
Eliminate remaining references to parent TheoryStrings...
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Add ProofNode data structure (#4311)
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Move regular expression inclusion test to RegExpEntail...
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Change option names --default-dag-thresh and --default...
commit
|
commitdiff
|
tree
2020-04-15
Andrew Reynolds
Split TermRegistry object from TheoryStrings (#4312)
commit
|
commitdiff
|
tree
next