projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Moving methods from quantifiers engine to quantifiers state (#5881)
[cvc5.git]
/
src
/
2021-02-13
Andrew Reynolds
Moving methods from quantifiers engine to quantifiers...
tree
|
commitdiff
2021-02-13
Mathias Preiner
Properly set up equality engine for BV bitblast solver...
tree
|
commitdiff
2021-02-12
Andrew Reynolds
Simplify and fix decision engine's handling of skolem...
tree
|
commitdiff
2021-02-12
Andrew Reynolds
(proof-new) Option to not automatically consider symmet...
tree
|
commitdiff
2021-02-11
Gereon Kremer
Make most methods of TheoryInferenceManager expect...
tree
|
commitdiff
2021-02-11
Gereon Kremer
Add InferenceId member to TheoryInference, adapt all...
tree
|
commitdiff
2021-02-11
Haniel Barbosa
[proof-new] Adding a proof-producing ensure literal...
tree
|
commitdiff
2021-02-11
Gereon Kremer
Merge InferenceIds into one enum (#5892)
tree
|
commitdiff
2021-02-11
Andrew Reynolds
Fix spurious assertion failure in regexp normalization...
tree
|
commitdiff
2021-02-11
Andrew Reynolds
Simplify interface for preprocessor (#5890)
tree
|
commitdiff
2021-02-10
Andrew Reynolds
Refactor term registration visitors (#5875)
tree
|
commitdiff
2021-02-10
Andrew Reynolds
Fix open proof for factoring lemma (#5885)
tree
|
commitdiff
2021-02-10
Andrew Reynolds
Simplify method for inferring proxy lemmas in strings...
tree
|
commitdiff
2021-02-10
Andrew Reynolds
Remove track instantiations infrastructure (#5883)
tree
|
commitdiff
2021-02-10
Andrew Reynolds
Optimize get skolems method (#5876)
tree
|
commitdiff
2021-02-10
Andrew Reynolds
Do not traverse quantifiers in term formula removal...
tree
|
commitdiff
2021-02-09
Mathias Preiner
cmake: Make Python3 default and improve toml error...
tree
|
commitdiff
2021-02-09
Andrew Reynolds
Eliminating dependencies from inst utils (#5882)
tree
|
commitdiff
2021-02-09
Andrew Reynolds
Make term database optionally SAT-context-dependent...
tree
|
commitdiff
2021-02-09
Haniel Barbosa
[quantifiers] Fix prenex computation (#5879)
tree
|
commitdiff
2021-02-08
Andrew Reynolds
Use quantifiers inference manager for lemma management...
tree
|
commitdiff
2021-02-08
Andrew Reynolds
Fix disequality between seq.unit terms (#5880)
tree
|
commitdiff
2021-02-08
Haniel Barbosa
Fix dumping of assertions for monolithic preprocessing...
tree
|
commitdiff
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
next