projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Fix regression option (#4680)
[cvc5.git]
/
src
/
theory
/
2020-07-02
Andrew Reynolds
(proof-new) Proof rule checkers run on skolem forms...
tree
|
commitdiff
2020-07-01
Andrew Reynolds
Add solver for integer AND (#4681)
tree
|
commitdiff
2020-07-01
Andrew Reynolds
Inferences and model construction taking into account...
tree
|
commitdiff
2020-07-01
Andrew Reynolds
(proof-new) Updates to evaluator (#4659)
tree
|
commitdiff
2020-07-01
Andrew Reynolds
(proof-new) Improve rewriter for WITNESS (#4661)
tree
|
commitdiff
2020-06-30
Andrew Reynolds
Fix normal form for re.comp (#4676)
tree
|
commitdiff
2020-06-30
Andrew Reynolds
Simplify quantifiers strategy for when to apply last...
tree
|
commitdiff
2020-06-30
Ying Sheng
Interpolation step 1 (#4638)
tree
|
commitdiff
2020-06-30
Andrew Reynolds
Add internal support for integer and operator (#4668)
tree
|
commitdiff
2020-06-29
Andres Noetzli
Make ExprManager constructor private (#4669)
tree
|
commitdiff
2020-06-28
Andrew Reynolds
Fix non-termination issues in simpleRegExpConsume ...
tree
|
commitdiff
2020-06-28
Alex Ozdemir
Proof Rules and Checker for Arithmetic (#4665)
tree
|
commitdiff
2020-06-25
Andrew Reynolds
(proof-new) Add TrustNode interfaces to OutputChannel...
tree
|
commitdiff
2020-06-25
Andrew Reynolds
Update option --nl-ext to enable/disable incremental...
tree
|
commitdiff
2020-06-23
Mathias Preiner
Add support for eqrange predicate (#4562)
tree
|
commitdiff
2020-06-22
Andrew Reynolds
(proof-new) Add REWRITE trust node kind. (#4624)
tree
|
commitdiff
2020-06-22
Andrew Reynolds
Add trascendental function kinds to list of unevaluated...
tree
|
commitdiff
2020-06-20
Andrew Reynolds
(proof-new) Make static methods in re-elim (#4623)
tree
|
commitdiff
2020-06-19
Andrew Reynolds
(proof-new) Updates to strings term registry (#4599)
tree
|
commitdiff
2020-06-19
Andrew Reynolds
Convert more uses of strings to words (#4584)
tree
|
commitdiff
2020-06-19
Andrew Reynolds
(proof-new) Split operator elimination from arithmetic...
tree
|
commitdiff
2020-06-19
Andrew Reynolds
Clean the header file of TheoryStrings (#4272)
tree
|
commitdiff
2020-06-19
Haniel Barbosa
Always rewrite boolean ITEs with constant then/else...
tree
|
commitdiff
2020-06-17
Andrew Reynolds
Do not traverse WITNESS for partial substitutions in...
tree
|
commitdiff
2020-06-17
Haniel Barbosa
Improve polynomial anyterm grammar (#3566)
tree
|
commitdiff
2020-06-16
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-06-16
Aina Niemetz
BV: Fix querying equality status in lazy bit-blaster...
tree
|
commitdiff
2020-06-16
Andrew Reynolds
(proof-new) Add quantifiers proof checker (#4593)
tree
|
commitdiff
2020-06-15
Haniel Barbosa
Support AND/OR definitions in lambda to array rewriting...
tree
|
commitdiff
2020-06-15
Aina Niemetz
BV: Add missing type check for BITVECTOR_REPEAT_OP...
tree
|
commitdiff
2020-06-15
Aina Niemetz
BV: Add missing type check for INT_TO_BITVECTOR. (...
tree
|
commitdiff
2020-06-15
Andrew Reynolds
Do RE derivation inference only for concrete constant...
tree
|
commitdiff
2020-06-13
Andrew Reynolds
Move sygus datatype utility functions to their own...
tree
|
commitdiff
2020-06-12
Andrew Reynolds
(proof-new) Minor updates to strings base solver (...
tree
|
commitdiff
2020-06-12
Andrew Reynolds
Cardinality-related inferences per type in theory of...
tree
|
commitdiff
2020-06-12
Andrew Reynolds
(proof-new) Split TheoryEngine (#4558)
tree
|
commitdiff
2020-06-12
Andrew Reynolds
Add rewrite for str.replace_re. (#4601)
tree
|
commitdiff
2020-06-11
Andrew Reynolds
(proof-new) Add eager proof generator utility. (#4592)
tree
|
commitdiff
2020-06-11
Andrew Reynolds
(proof-new) Remove arith-snorm option. (#4591)
tree
|
commitdiff
2020-06-10
Andrew Reynolds
(proof-new) Theory proof step buffer utility (#4580)
tree
|
commitdiff
2020-06-10
Andres Noetzli
Add support for str.replace_re/str.replace_re_all ...
tree
|
commitdiff
2020-06-09
Andrew Reynolds
(proof-new) Add trust node utility (#4588)
tree
|
commitdiff
2020-06-08
Andres Noetzli
Fix Coverity issues (#4587)
tree
|
commitdiff
2020-06-06
Andrew Reynolds
Use NlLemma utility for all lemmas in non-linear. ...
tree
|
commitdiff
2020-06-06
Andrew Reynolds
Smt2 parsing support for nested recursive datatypes...
tree
|
commitdiff
2020-06-05
Andrew Reynolds
Datatypes with nested recursion are not handled in...
tree
|
commitdiff
2020-06-05
Andrew Reynolds
(proof-new) Rename ProofSkolemCache to SkolemManager...
tree
|
commitdiff
2020-06-05
Andres Noetzli
Fix handling of Boolean term variables (#4550)
tree
|
commitdiff
2020-06-04
Andrew Reynolds
Add sygus datatype substitution utility method (#4390)
tree
|
commitdiff
2020-06-04
Andrew Reynolds
Fix abduction with datatypes (#4566)
tree
|
commitdiff
2020-06-04
Andrew Reynolds
Theory strings preprocess (#4534)
tree
|
commitdiff
2020-06-03
Haniel Barbosa
(proof-new) Adding rules and proof checker for EUF...
tree
|
commitdiff
2020-06-03
Haniel Barbosa
(proof-new) Adding rules and proof checker for Boolean...
tree
|
commitdiff
2020-06-03
Andrew Reynolds
(proof-new) Add builtin proof checker (#4537)
tree
|
commitdiff
2020-06-03
Andrew Reynolds
Update CEGQI to use lemma status instead of forcing...
tree
|
commitdiff
2020-06-03
Andrew Reynolds
Use prenex normal form when using cegqi-nested-qe ...
tree
|
commitdiff
2020-06-02
Andrew Reynolds
Fix scope issue with pulling ITEs in extended rewriter...
tree
|
commitdiff
2020-06-02
Andrew Reynolds
Do not handle universal quantification on functions...
tree
|
commitdiff
2020-06-01
Andrew Reynolds
Move non-linear files to src/theory/arith/nl (#4548)
tree
|
commitdiff
2020-06-01
Andrew Reynolds
Incorporate sequences into the word interface (#4543)
tree
|
commitdiff
2020-05-31
Andres Noetzli
Do not cache operator eliminations in arith (#4542)
tree
|
commitdiff
2020-05-30
Andrew Reynolds
Add the sequence type (#4539)
tree
|
commitdiff
2020-05-28
Andrew Reynolds
Fix term registry for constant case, simplify. (#4538)
tree
|
commitdiff
2020-05-27
Andrew Reynolds
Add the Expr-level sequence datatype (#4526)
tree
|
commitdiff
2020-05-26
Andrew Reynolds
Convert more uses of strings to words (#4527)
tree
|
commitdiff
2020-05-26
Andrew Reynolds
(proof-new) Updates to strings skolem cache. (#4524)
tree
|
commitdiff
2020-05-23
mudathirmahgoub
remove unused field d_emp_exp in TheorySetsPrivate...
tree
|
commitdiff
2020-05-23
Andrew Reynolds
Refactor operator elimination in arithmetic (#4519)
tree
|
commitdiff
2020-05-22
Andrew Reynolds
(proof-new) Add rewrite corresponding to regular expres...
tree
|
commitdiff
2020-05-22
Aina Niemetz
Add support for SAT solver Kissat. (#4514)
tree
|
commitdiff
2020-05-22
Andrew Reynolds
(proof-new) Minor update to strings solver state (...
tree
|
commitdiff
2020-05-21
Andrew Reynolds
Throw logic exception for equality between regular...
tree
|
commitdiff
2020-05-20
Andrew Reynolds
Normal form equality conflicts and uniqueness check...
tree
|
commitdiff
2020-05-20
Aina Niemetz
CegqiBv: Clean up after renaming options. (#4487)
tree
|
commitdiff
2020-05-20
Andrew Reynolds
Use debug-check-model to enable internal debugging...
tree
|
commitdiff
2020-05-20
Andrew Reynolds
Do not eliminate variables that are equal to unevaluata...
tree
|
commitdiff
2020-05-20
Andrew Reynolds
Fix cached free variable identifiers in sygus term...
tree
|
commitdiff
2020-05-19
mudathirmahgoub
Renamed operator CHOICE to WITNESS (#4207)
tree
|
commitdiff
2020-05-19
Andrew Reynolds
Use fresh variables when miniscoping (#4296)
tree
|
commitdiff
2020-05-19
Andres Noetzli
Make SolveEq and PlusCombineLikeTerms idempotent (...
tree
|
commitdiff
2020-04-30
Andrew Reynolds
Remove skolem share involving pre_first_ctn. (#4423)
tree
|
commitdiff
2020-04-30
Andrew Reynolds
Do not mark congruent terms are reduced (#4419)
tree
|
commitdiff
2020-04-29
Andrew Reynolds
Avoid circular dependencies for justifying reductions...
tree
|
commitdiff
2020-04-28
Andres Noetzli
Register lower bound for str.to_int (#4408)
tree
|
commitdiff
2020-04-28
Andrew Reynolds
Update cardinality in strings to unicode standard ...
tree
|
commitdiff
2020-04-26
Andrew Reynolds
Fix sets cardinality cycle rule (#4392)
tree
|
commitdiff
2020-04-23
Andres Noetzli
Introduce best content heuristic for strings (#4382)
tree
|
commitdiff
2020-04-23
Andres Noetzli
Strings: Register skolems before sending lemma (#4381)
tree
|
commitdiff
2020-04-22
Andrew Reynolds
Ensure disequality splits are processed as lemmas ...
tree
|
commitdiff
2020-04-22
Andres Noetzli
Reinstantiate support for conjunctions in facts (#4377)
tree
|
commitdiff
2020-04-21
Andrew Reynolds
Make option names related to CEGQI consistent (#4316)
tree
|
commitdiff
2020-04-20
Andrew Reynolds
Refactor inference manager in strings to be amenable...
tree
|
commitdiff
2020-04-18
Andrew Reynolds
Track inference id for pending facts in strings (#4331)
tree
|
commitdiff
2020-04-18
Haniel Barbosa
Improving EqProof printing (#4329)
tree
|
commitdiff
2020-04-17
Mathias Preiner
SyGuS instantiation quantifiers module (#3910)
tree
|
commitdiff
2020-04-16
Andrew Reynolds
Eliminate remaining references to parent TheoryStrings...
tree
|
commitdiff
2020-04-15
Andrew Reynolds
Move regular expression inclusion test to RegExpEntail...
tree
|
commitdiff
2020-04-15
Andrew Reynolds
Split TermRegistry object from TheoryStrings (#4312)
tree
|
commitdiff
2020-04-15
Andrew Reynolds
Do not mark string extended functions as eliminated...
tree
|
commitdiff
2020-04-15
Andrew Reynolds
Fix assertion in enumerative instantiation (#4313)
tree
|
commitdiff
next