projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Simplify interface to instantiate (#5926)
[cvc5.git]
/
src
/
theory
/
2021-02-19
Andrew Reynolds
Simplify interface to instantiate (#5926)
tree
|
commitdiff
2021-02-19
Andrew Reynolds
Fill in missing inference ids in datatypes theory ...
tree
|
commitdiff
2021-02-19
Andrew Reynolds
Refactoring theory inference process (#5920)
tree
|
commitdiff
2021-02-19
Andrew Reynolds
Fix rewrite for contains over replace (#5924)
tree
|
commitdiff
2021-02-19
Andrew Reynolds
Remove string stat for inferences (#5932)
tree
|
commitdiff
2021-02-19
Gereon Kremer
Cleanup of inferences in arithmetic theory (#5927)
tree
|
commitdiff
2021-02-18
Gereon Kremer
Add statistic for InferenceId to TheoryInferenceManager...
tree
|
commitdiff
2021-02-18
Gereon Kremer
Add InferenceIds for sets theory. (#5900)
tree
|
commitdiff
2021-02-18
Gereon Kremer
New InferenceIds for BV theory (#5909)
tree
|
commitdiff
2021-02-18
Andrew Reynolds
Document UF inferences (#5917)
tree
|
commitdiff
2021-02-18
Andrew Reynolds
Eliminate non-static members in term util (#5919)
tree
|
commitdiff
2021-02-18
Andrew Reynolds
Move first order model for full model check to own...
tree
|
commitdiff
2021-02-17
Andrew Reynolds
Move methods from term util to quantifiers registry...
tree
|
commitdiff
2021-02-17
Andrew Reynolds
Compute fact or lemma in datatypes prior to buffering...
tree
|
commitdiff
2021-02-17
Gereon Kremer
Use InferenceId in sep theory. (#5912)
tree
|
commitdiff
2021-02-17
Gereon Kremer
TheoryIds for UF theory. (#5901)
tree
|
commitdiff
2021-02-17
Gereon Kremer
Add InferenceIds for theory of arrays (#5910)
tree
|
commitdiff
2021-02-17
Gereon Kremer
Add InferenceId to buffered inference manager (#5911)
tree
|
commitdiff
2021-02-17
Mathias Preiner
Add bit-level propagation support to BV bitblast solver...
tree
|
commitdiff
2021-02-15
Gereon Kremer
Remove now obsolete sendLemmas and inferences stat...
tree
|
commitdiff
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-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
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-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-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
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-03
Mathias Preiner
Add BV solver bitblast. (#5851)
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-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
mudathirmahgoub
Fix BagsRewriter::rewriteUnionDisjoint (#5840)
tree
|
commitdiff
2021-01-30
Andrew Reynolds
Fix unguarded call to get representative (#5838)
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
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
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-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
next