projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Ensure uses of ground terms in triggers are preprocessed and registered (#5808)
[cvc5.git]
/
src
/
theory
/
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-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
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-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
mudathirmahgoub
Fix issue 5513 (#5757)
tree
|
commitdiff
2021-01-08
mudathirmahgoub
Rename getAntecedent to getPremises (#5754)
tree
|
commitdiff
2021-01-08
mudathirmahgoub
Add bags inference generator (#5731)
tree
|
commitdiff
2021-01-07
Gereon Kremer
Make sure polynomials are properly factorized in nl...
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
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
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
2020-12-18
Gereon Kremer
Add proof checker for nl tangent lemma (#5704)
tree
|
commitdiff
2020-12-18
Alex Ozdemir
Bugfix: proofs for props of non-normal arith lits ...
tree
|
commitdiff
2020-12-18
Gereon Kremer
(proof-new) Add proof for tangent plane lemmas (#5700)
tree
|
commitdiff
2020-12-18
Gereon Kremer
Add proof for split zero check. (#5699)
tree
|
commitdiff
2020-12-17
Gereon Kremer
Always consider rewritten lemmas for caching. (#5696)
tree
|
commitdiff
2020-12-17
Gereon Kremer
(proof-new) Prepare nonlinear extension and nl-ext...
tree
|
commitdiff
2020-12-16
Andrew Reynolds
Mark quantifier instantiations as needs justify (#5684)
tree
|
commitdiff
2020-12-16
mudathirmahgoub
Renamed InferInfo::getAntecedant to InferInfo::getAntec...
tree
|
commitdiff
2020-12-16
Andrew Reynolds
(proof-new) Use bound variable manager (#5679)
tree
|
commitdiff
2020-12-16
Andrew Reynolds
Move ownership of term formula removal to theory prepro...
tree
|
commitdiff
2020-12-15
Andrew Reynolds
Move trigger trie to own file (#5680)
tree
|
commitdiff
2020-12-15
Andrew Reynolds
Improvements related to quantifiers printing (#5678)
tree
|
commitdiff
2020-12-15
Andrew Reynolds
Proper expand definitions for sets (#5676)
tree
|
commitdiff
2020-12-15
Andrew Reynolds
Consolidate basic sygus utilities regarding sygus conje...
tree
|
commitdiff
2020-12-15
Andrew Reynolds
Fix datatypes compute ground value (#5671)
tree
|
commitdiff
2020-12-15
Andrew Reynolds
Remove bv divide by zero option (#5672)
tree
|
commitdiff
2020-12-14
Andrew Reynolds
Properly implement datatype selector triggers (#5624)
tree
|
commitdiff
2020-12-14
Andrew Reynolds
Fix and improve evaluator (#5563)
tree
|
commitdiff
2020-12-14
Andrew Reynolds
Fix SAT-context dependent issue in strings preregistrat...
tree
|
commitdiff
2020-12-11
Andrew Reynolds
Fix length assumption for deq norm emp rule (#5623)
tree
|
commitdiff
2020-12-10
Gereon Kremer
Refactor KindMap (#5646)
tree
|
commitdiff
2020-12-10
Gereon Kremer
Fixed a bunch of clang warnings. (#5637)
tree
|
commitdiff
2020-12-09
Aina Niemetz
Fix compiler warnings. (#5644)
tree
|
commitdiff
2020-12-09
Andrew Reynolds
(proof-new) Make theory preprocessor proofs self contai...
tree
|
commitdiff
2020-12-09
Andrew Reynolds
Make decision engine independent of AssertionsPipeline...
tree
|
commitdiff
2020-12-09
Gereon Kremer
Split initial exp lemma into separate lemmas. (#5622)
tree
|
commitdiff
2020-12-09
Andrew Reynolds
Ensure CEGQI is applied for parametric datatypes when...
tree
|
commitdiff
2020-12-09
Andrew Reynolds
Do not check FP at last call if not necessary (#5627)
tree
|
commitdiff
2020-12-08
Haniel Barbosa
[proof-new] Updating SAT proof to use MACRO_RESOLUTION...
tree
|
commitdiff
2020-12-08
Andrew Reynolds
Make term indices in the strings base solver aware...
tree
|
commitdiff
2020-12-08
Andrew Reynolds
Proper implementation of expand definitions for sequenc...
tree
|
commitdiff
2020-12-08
Andrew Reynolds
Fix collect model values for sequences of sequences...
tree
|
commitdiff
2020-12-08
Haniel Barbosa
[proof-new] Adding MACRO_RESOLUTION rule and updating...
tree
|
commitdiff
2020-12-08
Mathias Preiner
Add support for BV proofs with the simple bitblasting...
tree
|
commitdiff
2020-12-07
Andrew Reynolds
Fix and reenable fact vs lemma optimization in datatype...
tree
|
commitdiff
2020-12-07
makaimann
Add bitwise refinement mode for IAND (#5328)
tree
|
commitdiff
2020-12-07
Andrew Reynolds
Fix issue with free variables introduced by quantifier...
tree
|
commitdiff
2020-12-07
Gereon Kremer
Refactor initial phase of transcendental solver (#5599)
tree
|
commitdiff
2020-12-07
Andrew Reynolds
Do not expand theory definitions at the beginning of...
tree
|
commitdiff
2020-12-07
Andrew Reynolds
(proof-new) Split proof ensure closed checks to own...
tree
|
commitdiff
2020-12-03
Gereon Kremer
Use mkAnd where the number of children may be less...
tree
|
commitdiff
2020-12-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-12-02
Aina Niemetz
Rename macro Message to CVC4Message. (#5576)
tree
|
commitdiff
2020-12-02
Andrew Reynolds
(proof-new) Proofs for expand definitions (#5562)
tree
|
commitdiff
2020-12-02
Andrew Reynolds
Remove assertion related to CEGQI dependency lemmas...
tree
|
commitdiff
2020-12-01
Andres Noetzli
Improve rewriting of str.<= (#4848)
tree
|
commitdiff
2020-12-01
Gereon Kremer
Refactor transcendental solver (#5539)
tree
|
commitdiff
2020-12-01
Andrew Reynolds
More fixes for quantifier elimination (#5533)
tree
|
commitdiff
2020-11-30
Aina Niemetz
fp_converter: Properly separate out symbolic glue code...
tree
|
commitdiff
2020-11-30
Andrew Reynolds
Remove includes for old API from internal code (#5536)
tree
|
commitdiff
2020-11-30
Andrew Reynolds
(proof-new) Proofs for regular expression elimination...
tree
|
commitdiff
2020-11-26
Gereon Kremer
Make CAD solver work for empty set of assertions (...
tree
|
commitdiff
2020-11-26
Andrew Reynolds
Fully decouple SmtEngine and the Expr layer (#5532)
tree
|
commitdiff
2020-11-26
Andrew Reynolds
Fix missed case of theory preprocessing (#5531)
tree
|
commitdiff
2020-11-26
Andrew Reynolds
Disable fact vs lemma optimization in datatypes for...
tree
|
commitdiff
next