projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2021-02-18
Gereon Kremer
Add InferenceIds for sets theory. (#5900)
commit
|
commitdiff
|
tree
2021-02-18
Gereon Kremer
New InferenceIds for BV theory (#5909)
commit
|
commitdiff
|
tree
2021-02-18
Andrew Reynolds
Document UF inferences (#5917)
commit
|
commitdiff
|
tree
2021-02-18
Andrew Reynolds
Eliminate non-static members in term util (#5919)
commit
|
commitdiff
|
tree
2021-02-18
Andrew Reynolds
Move first order model for full model check to own...
commit
|
commitdiff
|
tree
2021-02-17
Andrew Reynolds
Move methods from term util to quantifiers registry...
commit
|
commitdiff
|
tree
2021-02-17
Andrew Reynolds
Compute fact or lemma in datatypes prior to buffering...
commit
|
commitdiff
|
tree
2021-02-17
Gereon Kremer
Use InferenceId in sep theory. (#5912)
commit
|
commitdiff
|
tree
2021-02-17
Gereon Kremer
TheoryIds for UF theory. (#5901)
commit
|
commitdiff
|
tree
2021-02-17
Gereon Kremer
Add InferenceIds for theory of arrays (#5910)
commit
|
commitdiff
|
tree
2021-02-17
Gereon Kremer
Add InferenceId to buffered inference manager (#5911)
commit
|
commitdiff
|
tree
2021-02-17
Gereon Kremer
Add new IntegralHistogramStat (#5898)
commit
|
commitdiff
|
tree
2021-02-17
Mathias Preiner
Add bit-level propagation support to BV bitblast solver...
commit
|
commitdiff
|
tree
2021-02-16
Aina Niemetz
google test: parser: Migrate parser_builder_black....
commit
|
commitdiff
|
tree
2021-02-15
Gereon Kremer
Remove now obsolete sendLemmas and inferences stat...
commit
|
commitdiff
|
tree
2021-02-13
Andrew Reynolds
Moving methods from quantifiers engine to quantifiers...
commit
|
commitdiff
|
tree
2021-02-13
Mathias Preiner
Properly set up equality engine for BV bitblast solver...
commit
|
commitdiff
|
tree
2021-02-12
Andrew Reynolds
Simplify and fix decision engine's handling of skolem...
commit
|
commitdiff
|
tree
2021-02-12
Andrew Reynolds
(proof-new) Option to not automatically consider symmet...
commit
|
commitdiff
|
tree
2021-02-11
Aina Niemetz
google test: parser: Migrate parser_black. (#5886)
commit
|
commitdiff
|
tree
2021-02-11
Gereon Kremer
Make most methods of TheoryInferenceManager expect...
commit
|
commitdiff
|
tree
2021-02-11
Gereon Kremer
Add InferenceId member to TheoryInference, adapt all...
commit
|
commitdiff
|
tree
2021-02-11
Haniel Barbosa
[proof-new] Adding a proof-producing ensure literal...
commit
|
commitdiff
|
tree
2021-02-11
Gereon Kremer
Merge InferenceIds into one enum (#5892)
commit
|
commitdiff
|
tree
2021-02-11
Andrew Reynolds
Fix spurious assertion failure in regexp normalization...
commit
|
commitdiff
|
tree
2021-02-11
Andrew Reynolds
Simplify interface for preprocessor (#5890)
commit
|
commitdiff
|
tree
2021-02-10
Andrew Reynolds
Refactor term registration visitors (#5875)
commit
|
commitdiff
|
tree
2021-02-10
Andrew Reynolds
Fix open proof for factoring lemma (#5885)
commit
|
commitdiff
|
tree
2021-02-10
Andrew Reynolds
Simplify method for inferring proxy lemmas in strings...
commit
|
commitdiff
|
tree
2021-02-10
Andrew Reynolds
Remove track instantiations infrastructure (#5883)
commit
|
commitdiff
|
tree
2021-02-10
Andrew Reynolds
Optimize get skolems method (#5876)
commit
|
commitdiff
|
tree
2021-02-10
Andrew Reynolds
Do not traverse quantifiers in term formula removal...
commit
|
commitdiff
|
tree
2021-02-09
Mathias Preiner
cmake: Make Python3 default and improve toml error...
commit
|
commitdiff
|
tree
2021-02-09
Andrew Reynolds
Eliminating dependencies from inst utils (#5882)
commit
|
commitdiff
|
tree
2021-02-09
Andrew Reynolds
Make term database optionally SAT-context-dependent...
commit
|
commitdiff
|
tree
2021-02-09
Aina Niemetz
google test: expr: Migrate node_manager_black. (#5857)
commit
|
commitdiff
|
tree
2021-02-09
Aina Niemetz
google test: main: Migrate interactive_shell_black...
commit
|
commitdiff
|
tree
2021-02-09
Aina Niemetz
google test: expr: Migrate type_cardinality_black....
commit
|
commitdiff
|
tree
2021-02-09
Aina Niemetz
google test: expr: Migrate node_self_iterator_black...
commit
|
commitdiff
|
tree
2021-02-09
Haniel Barbosa
[quantifiers] Fix prenex computation (#5879)
commit
|
commitdiff
|
tree
2021-02-09
Aina Niemetz
google test: expr: Migrate type_node_white. (#5872)
commit
|
commitdiff
|
tree
2021-02-08
Andrew Reynolds
Use quantifiers inference manager for lemma management...
commit
|
commitdiff
|
tree
2021-02-08
Andrew Reynolds
Fix disequality between seq.unit terms (#5880)
commit
|
commitdiff
|
tree
2021-02-08
Aina Niemetz
google test: expr: Migrate node_white. (#5869)
commit
|
commitdiff
|
tree
2021-02-08
Haniel Barbosa
Fix dumping of assertions for monolithic preprocessing...
commit
|
commitdiff
|
tree
2021-02-08
Andrew Reynolds
Remove support for inst closure (#5874)
commit
|
commitdiff
|
tree
2021-02-08
Aina Niemetz
Use consistent names for fixtures in unit tests. (...
commit
|
commitdiff
|
tree
2021-02-08
Aina Niemetz
google test: expr: Migrate node_traversal_black. (...
commit
|
commitdiff
|
tree
2021-02-08
Andrew Reynolds
Avoid spurious traversal of terms during preregistratio...
commit
|
commitdiff
|
tree
2021-02-06
Andrew Reynolds
Do not combine theories if theory engine needs check...
commit
|
commitdiff
|
tree
2021-02-05
Aina Niemetz
google test: expr: Migrate symbol_table_black. (#5870)
commit
|
commitdiff
|
tree
2021-02-05
Andrew Reynolds
Minor cleaning of quantifiers engine (#5858)
commit
|
commitdiff
|
tree
2021-02-05
Aina Niemetz
google test: expr: Migrate node_manager_white. (#5864)
commit
|
commitdiff
|
tree
2021-02-05
Aina Niemetz
Remove obsolete include from node_black unit test....
commit
|
commitdiff
|
tree
2021-02-05
Aina Niemetz
google test: expr: Migrate node_builder_black. (#5855)
commit
|
commitdiff
|
tree
2021-02-05
Andrew Reynolds
Miscellaneous cleaning in theory engine (#5854)
commit
|
commitdiff
|
tree
2021-02-04
yoni206
Adding an option to optimize polite combination for...
commit
|
commitdiff
|
tree
2021-02-04
Andrew Reynolds
Introduce quantifiers registry utility (#5829)
commit
|
commitdiff
|
tree
2021-02-04
yoni206
Clarifying documentation of `--static-binary` (#5844)
commit
|
commitdiff
|
tree
2021-02-04
Andrew Reynolds
Eliminate equality query dependence on quantifiers...
commit
|
commitdiff
|
tree
2021-02-04
Haniel Barbosa
[proof-new] Catch trivial cycles in SAT proof generatio...
commit
|
commitdiff
|
tree
2021-02-03
Mathias Preiner
Add BV solver bitblast. (#5851)
commit
|
commitdiff
|
tree
2021-02-03
Haniel Barbosa
[proof-new] Fix MACRO_RESOLUTION expansion for singleto...
commit
|
commitdiff
|
tree
2021-02-02
Andrew Reynolds
(proof-new) Miscellaneous fixes and regressions (#5841)
commit
|
commitdiff
|
tree
2021-02-02
Andrew Reynolds
(proof-new) Refactor theory preprocessing (#5835)
commit
|
commitdiff
|
tree
2021-02-02
Andrew Reynolds
Remove quantifiers regression from decision folder...
commit
|
commitdiff
|
tree
2021-02-02
Andrew Reynolds
Cleanup some includes (#5847)
commit
|
commitdiff
|
tree
2021-02-02
Andrew Reynolds
Improvements for NL traces (#5846)
commit
|
commitdiff
|
tree
2021-02-02
Haniel Barbosa
[proof-new] Fix bug in expansion of MACRO_RESOLUTION...
commit
|
commitdiff
|
tree
2021-02-01
Andrew Reynolds
Eliminate PREPROCESS lemma property (#5827)
commit
|
commitdiff
|
tree
2021-02-01
Andrew Reynolds
Simplify alpha equivalence module (#5839)
commit
|
commitdiff
|
tree
2021-02-01
Abdalrhman...
Avoid calling the printers while converting sexpr to...
commit
|
commitdiff
|
tree
2021-02-01
mudathirmahgoub
Fix BagsRewriter::rewriteUnionDisjoint (#5840)
commit
|
commitdiff
|
tree
2021-01-30
Andrew Reynolds
Fix unguarded call to get representative (#5838)
commit
|
commitdiff
|
tree
2021-01-29
Haniel Barbosa
[proof-new] Connecting new unsat cores (#5834)
commit
|
commitdiff
|
tree
2021-01-29
mudathirmahgoub
Add bag inferences for operators: intersection, duplica...
commit
|
commitdiff
|
tree
2021-01-29
Andrew Reynolds
(proof-new) Distinguish pre vs post rewrites in term...
commit
|
commitdiff
|
tree
2021-01-28
Andrew Reynolds
Reorganize calls to quantifiers engine from SmtEngine...
commit
|
commitdiff
|
tree
2021-01-28
mudathirmahgoub
Remove regex header from cvc4cpp.cpp (#5826)
commit
|
commitdiff
|
tree
2021-01-28
Andrew Reynolds
Simplify lemma interface (#5819)
commit
|
commitdiff
|
tree
2021-01-28
Andrew Reynolds
Use standard equality engine information in quantifiers...
commit
|
commitdiff
|
tree
2021-01-28
Andrew Reynolds
Always theory-preprocess lemmas (#5817)
commit
|
commitdiff
|
tree
2021-01-27
Andrew Reynolds
Add option for whether to filter candidate rewrite...
commit
|
commitdiff
|
tree
2021-01-27
Andrew Reynolds
Split pattern term selector from trigger (#5811)
commit
|
commitdiff
|
tree
2021-01-27
Andrew Reynolds
(proof-new) Improvements to quantifiers engine and...
commit
|
commitdiff
|
tree
2021-01-27
Alex Ozdemir
Thread proofs through arith channels & similar (#5818)
commit
|
commitdiff
|
tree
2021-01-27
Andrew Reynolds
Use term canonizer utility locally in quantifiers ...
commit
|
commitdiff
|
tree
2021-01-27
Andrew Reynolds
Use standard conflict mechanism in quantifiers state...
commit
|
commitdiff
|
tree
2021-01-26
Andrew Reynolds
Introduce quantifiers inference manager (#5821)
commit
|
commitdiff
|
tree
2021-01-26
Andrew Reynolds
Remove deprecated quantifiers modules (#5820)
commit
|
commitdiff
|
tree
2021-01-26
Andrew Reynolds
Refactor quantifiers engine initialization (#5813)
commit
|
commitdiff
|
tree
2021-01-26
Haniel Barbosa
Reestablishing support for define-sort (#5810)
commit
|
commitdiff
|
tree
2021-01-26
Alex Ozdemir
Add proofs to TheoryArithPrivate::propagate (#5812)
commit
|
commitdiff
|
tree
2021-01-25
mudathirmahgoub
Refactor bags::SolverState (#5783)
commit
|
commitdiff
|
tree
2021-01-25
Andrew Reynolds
Ensure uses of ground terms in triggers are preprocesse...
commit
|
commitdiff
|
tree
2021-01-25
Andrew Reynolds
Split inst match generator into multiple files (#5805)
commit
|
commitdiff
|
tree
2021-01-25
Andrew Reynolds
Split E-matching strategies to own files (#5807)
commit
|
commitdiff
|
tree
2021-01-25
mudathirmahgoub
rename InferInfo::d_newSkolem to InferInfo::d_skolems...
commit
|
commitdiff
|
tree
2021-01-24
Andrew Reynolds
Initial cleaning of e-matching instantiation strategy...
commit
|
commitdiff
|
tree
2021-01-24
Andrew Reynolds
Initial cleaning of triggers (#5795)
commit
|
commitdiff
|
tree
next