projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Remove support for inst closure (#5874)
[cvc5.git]
/
src
/
2021-02-08
Andrew Reynolds
Remove support for inst closure (#5874)
tree
|
commitdiff
2021-02-08
Andrew Reynolds
Avoid spurious traversal of terms during preregistratio...
tree
|
commitdiff
2021-02-06
Andrew Reynolds
Do not combine theories if theory engine needs check...
tree
|
commitdiff
2021-02-05
Andrew Reynolds
Minor cleaning of quantifiers engine (#5858)
tree
|
commitdiff
2021-02-05
Andrew Reynolds
Miscellaneous cleaning in theory engine (#5854)
tree
|
commitdiff
2021-02-04
yoni206
Adding an option to optimize polite combination for...
tree
|
commitdiff
2021-02-04
Andrew Reynolds
Introduce quantifiers registry utility (#5829)
tree
|
commitdiff
2021-02-04
Andrew Reynolds
Eliminate equality query dependence on quantifiers...
tree
|
commitdiff
2021-02-04
Haniel Barbosa
[proof-new] Catch trivial cycles in SAT proof generatio...
tree
|
commitdiff
2021-02-03
Mathias Preiner
Add BV solver bitblast. (#5851)
tree
|
commitdiff
2021-02-03
Haniel Barbosa
[proof-new] Fix MACRO_RESOLUTION expansion for singleto...
tree
|
commitdiff
2021-02-02
Andrew Reynolds
(proof-new) Miscellaneous fixes and regressions (#5841)
tree
|
commitdiff
2021-02-02
Andrew Reynolds
(proof-new) Refactor theory preprocessing (#5835)
tree
|
commitdiff
2021-02-02
Andrew Reynolds
Cleanup some includes (#5847)
tree
|
commitdiff
2021-02-02
Andrew Reynolds
Improvements for NL traces (#5846)
tree
|
commitdiff
2021-02-02
Haniel Barbosa
[proof-new] Fix bug in expansion of MACRO_RESOLUTION...
tree
|
commitdiff
2021-02-01
Andrew Reynolds
Eliminate PREPROCESS lemma property (#5827)
tree
|
commitdiff
2021-02-01
Andrew Reynolds
Simplify alpha equivalence module (#5839)
tree
|
commitdiff
2021-02-01
Abdalrhman Mohamed
Avoid calling the printers while converting sexpr to...
tree
|
commitdiff
2021-02-01
mudathirmahgoub
Fix BagsRewriter::rewriteUnionDisjoint (#5840)
tree
|
commitdiff
2021-01-30
Andrew Reynolds
Fix unguarded call to get representative (#5838)
tree
|
commitdiff
2021-01-29
Haniel Barbosa
[proof-new] Connecting new unsat cores (#5834)
tree
|
commitdiff
2021-01-29
mudathirmahgoub
Add bag inferences for operators: intersection, duplica...
tree
|
commitdiff
2021-01-29
Andrew Reynolds
(proof-new) Distinguish pre vs post rewrites in term...
tree
|
commitdiff
2021-01-28
Andrew Reynolds
Reorganize calls to quantifiers engine from SmtEngine...
tree
|
commitdiff
2021-01-28
mudathirmahgoub
Remove regex header from cvc4cpp.cpp (#5826)
tree
|
commitdiff
2021-01-28
Andrew Reynolds
Simplify lemma interface (#5819)
tree
|
commitdiff
2021-01-28
Andrew Reynolds
Use standard equality engine information in quantifiers...
tree
|
commitdiff
2021-01-28
Andrew Reynolds
Always theory-preprocess lemmas (#5817)
tree
|
commitdiff
2021-01-27
Andrew Reynolds
Add option for whether to filter candidate rewrite...
tree
|
commitdiff
2021-01-27
Andrew Reynolds
Split pattern term selector from trigger (#5811)
tree
|
commitdiff
2021-01-27
Andrew Reynolds
(proof-new) Improvements to quantifiers engine and...
tree
|
commitdiff
2021-01-27
Alex Ozdemir
Thread proofs through arith channels & similar (#5818)
tree
|
commitdiff
2021-01-27
Andrew Reynolds
Use term canonizer utility locally in quantifiers ...
tree
|
commitdiff
2021-01-27
Andrew Reynolds
Use standard conflict mechanism in quantifiers state...
tree
|
commitdiff
2021-01-26
Andrew Reynolds
Introduce quantifiers inference manager (#5821)
tree
|
commitdiff
2021-01-26
Andrew Reynolds
Remove deprecated quantifiers modules (#5820)
tree
|
commitdiff
2021-01-26
Andrew Reynolds
Refactor quantifiers engine initialization (#5813)
tree
|
commitdiff
2021-01-26
Haniel Barbosa
Reestablishing support for define-sort (#5810)
tree
|
commitdiff
2021-01-26
Alex Ozdemir
Add proofs to TheoryArithPrivate::propagate (#5812)
tree
|
commitdiff
2021-01-25
mudathirmahgoub
Refactor bags::SolverState (#5783)
tree
|
commitdiff
2021-01-25
Andrew Reynolds
Ensure uses of ground terms in triggers are preprocesse...
tree
|
commitdiff
2021-01-25
Andrew Reynolds
Split inst match generator into multiple files (#5805)
tree
|
commitdiff
2021-01-25
Andrew Reynolds
Split E-matching strategies to own files (#5807)
tree
|
commitdiff
2021-01-25
mudathirmahgoub
rename InferInfo::d_newSkolem to InferInfo::d_skolems...
tree
|
commitdiff
2021-01-24
Andrew Reynolds
Initial cleaning of e-matching instantiation strategy...
tree
|
commitdiff
2021-01-24
Andrew Reynolds
Initial cleaning of triggers (#5795)
tree
|
commitdiff
2021-01-24
Andrew Reynolds
Initial cleaning of inst match generator (#5794)
tree
|
commitdiff
2021-01-24
Andrew Reynolds
(proof-new) Instantiation list utility (#5768)
tree
|
commitdiff
2021-01-24
Andrew Reynolds
Add interface for getting preprocessed term (#5798)
tree
|
commitdiff
2021-01-22
Haniel Barbosa
[proof-new] Expanding MACRO_RESOLUTION in post-processi...
tree
|
commitdiff
2021-01-21
Andrew Reynolds
Add div, mod, abs in non-strict parsing mode (#5793)
tree
|
commitdiff
2021-01-21
Alex Ozdemir
arith: Proofs for Diophantine cuts (#5792)
tree
|
commitdiff
2021-01-20
Andrew Reynolds
Refactoring the single invocation solver (#5706)
tree
|
commitdiff
2021-01-20
Andrew Reynolds
Fix type issues with relevant domain computation (...
tree
|
commitdiff
2021-01-20
Andrew Reynolds
Fix corner case of wrongly applied selector as trigger...
tree
|
commitdiff
2021-01-20
Andrew Reynolds
Do not track processed in remove term formulas loop...
tree
|
commitdiff
2021-01-20
Aina Niemetz
SMT2 parser: Do not add non-linear symbols for linear...
tree
|
commitdiff
2021-01-20
Andrew Reynolds
Use arbitrary ground term assignment for sorts where...
tree
|
commitdiff
2021-01-19
Alex Ozdemir
Implement proofs for arith BRAB lemmas (#5784)
tree
|
commitdiff
2021-01-15
Andrew Reynolds
Implement --no-strings-lazy-pp as a preprocessing pass...
tree
|
commitdiff
2021-01-14
Andrew Reynolds
Updates to theory preprocess equality (#5776)
tree
|
commitdiff
2021-01-13
Andrew Reynolds
Split eager solver from strings solver state (#5775)
tree
|
commitdiff
2021-01-13
Andrew Reynolds
Do not call ppRewrite on Boolean equalities (#5762)
tree
|
commitdiff
2021-01-12
yoni206
Foreign theory rewrite option (#5763)
tree
|
commitdiff
2021-01-11
Andrew Reynolds
Merge theory registrar and theory proxy (#5758)
tree
|
commitdiff
2021-01-11
Andrew Reynolds
Further simplifications in preparation for removing...
tree
|
commitdiff
2021-01-11
Andrew Reynolds
Remove extended rewrite for arithmetic (#5760)
tree
|
commitdiff
2021-01-09
yoni206
Strings arith checks preprocessing pass: step 2 (#5750)
tree
|
commitdiff
2021-01-09
mudathirmahgoub
Fix issue 5513 (#5757)
tree
|
commitdiff
2021-01-08
mudathirmahgoub
Rename getAntecedent to getPremises (#5754)
tree
|
commitdiff
2021-01-08
Haniel Barbosa
[proof-new] Implementing getProof in the API and SMT...
tree
|
commitdiff
2021-01-08
mudathirmahgoub
Add bags inference generator (#5731)
tree
|
commitdiff
2021-01-08
yoni206
bv-to-int: avoid binarizing nodes twice (#5749)
tree
|
commitdiff
2021-01-07
Gereon Kremer
Make sure polynomials are properly factorized in nl...
tree
|
commitdiff
2021-01-07
Haniel Barbosa
Remove dependency on expression layer in TPTP parser...
tree
|
commitdiff
2021-01-07
Haniel Barbosa
Fix warning in TPTP parser (#5752)
tree
|
commitdiff
2021-01-06
yoni206
strings arith checks preprocessing pass: step 1 (#5747)
tree
|
commitdiff
2021-01-06
Andrew Reynolds
Add new interfaces to term formula removal and theory...
tree
|
commitdiff
2021-01-05
yoni206
Adding str.len to triggers (#5746)
tree
|
commitdiff
2021-01-05
Andrew Reynolds
Remove a few miscellaneous references to the expr layer...
tree
|
commitdiff
2020-12-24
Haniel Barbosa
[proof-new] Only use old proofs for unsat cores if...
tree
|
commitdiff
2020-12-23
Haniel Barbosa
Dumping unsat cores after check-sat-assuming/QUERY...
tree
|
commitdiff
2020-12-23
Andrew Reynolds
Add option to track and notify from CNF stream (#5708)
tree
|
commitdiff
2020-12-23
Andrew Reynolds
Remove quant EPR option (#5716)
tree
|
commitdiff
2020-12-23
Haniel Barbosa
[proof-new] Adding a manager for the new unsat cores...
tree
|
commitdiff
2020-12-23
Andrew Reynolds
(proof-new) Miscelleneous fixes from proof-new (#5714)
tree
|
commitdiff
2020-12-23
Gereon Kremer
Add proofs for nonlinear sign lemmas. (#5707)
tree
|
commitdiff
2020-12-23
Andrew Reynolds
Minor simplification to Theory::theoryOf (#5719)
tree
|
commitdiff
2020-12-22
yoni206
Delete duplicated code (#5718)
tree
|
commitdiff
2020-12-22
Andrew Reynolds
Make theory preprocess rewrite equalities a preprocessi...
tree
|
commitdiff
2020-12-22
Andrew Reynolds
Remove preregister instantiation heuristic (#5713)
tree
|
commitdiff
2020-12-21
Gereon Kremer
Add proof for pi bound lemma (#5709)
tree
|
commitdiff
2020-12-21
Andrew Reynolds
Move ownership of theory preprocessor to TheoryProxy...
tree
|
commitdiff
2020-12-21
Gereon Kremer
Add proof for sine shift lemmas. (#5710)
tree
|
commitdiff
2020-12-21
Gereon Kremer
(proof-new) Make nl-ext factoring lemmas proof producin...
tree
|
commitdiff
2020-12-21
Andrew Reynolds
Eliminate recursion from the internals of term formula...
tree
|
commitdiff
2020-12-21
Andrew Reynolds
Fix issue with selector triggers (#5689)
tree
|
commitdiff
2020-12-18
Gereon Kremer
(proof-new) Setup proof infrastructure for transcendent...
tree
|
commitdiff
2020-12-18
Andrew Reynolds
Simplify internal API for sygus (#5687)
tree
|
commitdiff
next