projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first
⋅
prev
⋅
next
Remove quantifiers regression from decision folder (#5830)
2020-12-17
Andrew Reynolds
Simplify term formula removal interface (#5695)
commit
|
commitdiff
|
tree
2020-12-17
Andrew Reynolds
Simplify and fix check models (#5685)
commit
|
commitdiff
|
tree
2020-12-17
Haniel Barbosa
[proof-new] Only use old proof code for unsat cores...
commit
|
commitdiff
|
tree
2020-12-16
Andrew Reynolds
Simplify preprocessing (#5647)
commit
|
commitdiff
|
tree
2020-12-16
Andrew Reynolds
Mark quantifier instantiations as needs justify (#5684)
commit
|
commitdiff
|
tree
2020-12-16
Andrew Reynolds
Simplify synth-fun printer (#5682)
commit
|
commitdiff
|
tree
2020-12-16
mudathirmahgoub
Renamed InferInfo::getAntecedant to InferInfo::getAntecedent...
commit
|
commitdiff
|
tree
2020-12-16
Andrew Reynolds
(proof-new) Use bound variable manager (#5679)
commit
|
commitdiff
|
tree
2020-12-16
Andrew Reynolds
Move ownership of term formula removal to theory preprocesso...
commit
|
commitdiff
|
tree
2020-12-16
Andrew Reynolds
Use uint64 utility when parsing tuple selectors in...
commit
|
commitdiff
|
tree
2020-12-15
Andrew Reynolds
Move trigger trie to own file (#5680)
commit
|
commitdiff
|
tree
2020-12-15
Andrew Reynolds
Improvements related to quantifiers printing (#5678)
commit
|
commitdiff
|
tree
2020-12-15
Andrew Reynolds
Proper expand definitions for sets (#5676)
commit
|
commitdiff
|
tree
2020-12-15
Andrew Reynolds
Consolidate basic sygus utilities regarding sygus conjecture...
commit
|
commitdiff
|
tree
2020-12-15
Andrew Reynolds
Fix datatypes compute ground value (#5671)
commit
|
commitdiff
|
tree
2020-12-15
Andrew Reynolds
Remove bv divide by zero option (#5672)
commit
|
commitdiff
|
tree
2020-12-15
Gereon Kremer
Add getters to retrieve constants from api::Term (...
commit
|
commitdiff
|
tree
2020-12-14
Haniel Barbosa
[proof-new] Making the CDCL(T) Minisat proof producing...
commit
|
commitdiff
|
tree
2020-12-14
Haniel Barbosa
[proof-new] Make prop engine proof producing (#5667)
commit
|
commitdiff
|
tree
2020-12-14
Andrew Reynolds
Properly implement datatype selector triggers (#5624)
commit
|
commitdiff
|
tree
2020-12-14
Haniel Barbosa
[proof-new] Updating interfaces between prop engine...
commit
|
commitdiff
|
tree
2020-12-14
Andrew Reynolds
(proof-new) Add bound variable manager (#5655)
commit
|
commitdiff
|
tree
2020-12-14
Andrew Reynolds
Fix and improve evaluator (#5563)
commit
|
commitdiff
|
tree
2020-12-14
Andrew Reynolds
Fix SAT-context dependent issue in strings preregistration...
commit
|
commitdiff
|
tree
2020-12-12
Andrew Reynolds
Flush statistics through NodeManager in SmtEngine ...
commit
|
commitdiff
|
tree
2020-12-11
yoni206
bv-to-int: new tests from an issue (#5654)
commit
|
commitdiff
|
tree
2020-12-11
Haniel Barbosa
[proof-new] Updating theory proxy to new proof infrastructu...
commit
|
commitdiff
|
tree
2020-12-11
Andrew Reynolds
Fix length assumption for deq norm emp rule (#5623)
commit
|
commitdiff
|
tree
2020-12-10
Gereon Kremer
Refactor KindMap (#5646)
commit
|
commitdiff
|
tree
2020-12-10
Aina Niemetz
google test: expr: Migrate node_algorithm_black. (...
commit
|
commitdiff
|
tree
2020-12-10
Andrew Reynolds
Refactor regressions (#5639)
commit
|
commitdiff
|
tree
2020-12-10
Aina Niemetz
google test: expr: Migrate kind_black. (#5634)
commit
|
commitdiff
|
tree
2020-12-10
Gereon Kremer
Fixed a bunch of clang warnings. (#5637)
commit
|
commitdiff
|
tree
2020-12-09
Aina Niemetz
Fix compiler warnings. (#5644)
commit
|
commitdiff
|
tree
2020-12-09
Andrew Reynolds
(proof-new) Make theory preprocessor proofs self contained...
commit
|
commitdiff
|
tree
2020-12-09
Aina Niemetz
google test: expr: Migrate kind_map_black. (#5640)
commit
|
commitdiff
|
tree
2020-12-09
Aina Niemetz
kind_map: Remove unused Accessor class. (#5641)
commit
|
commitdiff
|
tree
2020-12-09
Aina Niemetz
google test: expr: Migrate attribute_white. (#5632)
commit
|
commitdiff
|
tree
2020-12-09
Andrew Reynolds
Make decision engine independent of AssertionsPipeline...
commit
|
commitdiff
|
tree
2020-12-09
Andrew Reynolds
Remove obsolete regressions (#5633)
commit
|
commitdiff
|
tree
2020-12-09
Aina Niemetz
google test: context: Migrate context_white. (#5630)
commit
|
commitdiff
|
tree
2020-12-09
Gereon Kremer
Split initial exp lemma into separate lemmas. (#5622)
commit
|
commitdiff
|
tree
2020-12-09
Aina Niemetz
Delete obsolete unit tests for Expr and ExprManager...
commit
|
commitdiff
|
tree
2020-12-09
Andrew Reynolds
Ensure CEGQI is applied for parametric datatypes when...
commit
|
commitdiff
|
tree
2020-12-09
Andrew Reynolds
Do not check FP at last call if not necessary (#5627)
commit
|
commitdiff
|
tree
2020-12-09
Aina Niemetz
ite_utilities: Fix infinite loop in compressTerm. ...
commit
|
commitdiff
|
tree
2020-12-09
yoni206
update doc (#5619)
commit
|
commitdiff
|
tree
2020-12-08
Aina Niemetz
google test: context: Migrate context_mm_black. (#5592)
commit
|
commitdiff
|
tree
2020-12-08
Aina Niemetz
google test: context: Migrate context_black. (#5587)
commit
|
commitdiff
|
tree
2020-12-08
Gereon Kremer
Add regression from #1978. (#5552)
commit
|
commitdiff
|
tree
2020-12-08
Abdalrhman Mohamed
Fix a bug with synth-fun printer (#5512)
commit
|
commitdiff
|
tree
2020-12-08
Haniel Barbosa
[proof-new] Updating SAT proof to use MACRO_RESOLUTION...
commit
|
commitdiff
|
tree
2020-12-08
yoni206
bv-to-int: Expand definitions of bvudiv and bvurem...
commit
|
commitdiff
|
tree
2020-12-08
Andrew Reynolds
Make term indices in the strings base solver aware...
commit
|
commitdiff
|
tree
2020-12-08
Andrew Reynolds
Proper implementation of expand definitions for sequences...
commit
|
commitdiff
|
tree
2020-12-08
Andrew Reynolds
Fix collect model values for sequences of sequences...
commit
|
commitdiff
|
tree
2020-12-08
Haniel Barbosa
[proof-new] Adding MACRO_RESOLUTION rule and updating...
commit
|
commitdiff
|
tree
2020-12-08
Mathias Preiner
Add support for BV proofs with the simple bitblasting...
commit
|
commitdiff
|
tree
2020-12-08
Mathias Preiner
Disable algebraic BV subtheory by default and make...
commit
|
commitdiff
|
tree
2020-12-07
Andrew Reynolds
Fix and reenable fact vs lemma optimization in datatypes...
commit
|
commitdiff
|
tree
2020-12-07
makaimann
Add bitwise refinement mode for IAND (#5328)
commit
|
commitdiff
|
tree
2020-12-07
Andrew Reynolds
Fix issue with free variables introduced by quantifier...
commit
|
commitdiff
|
tree
2020-12-07
Gereon Kremer
Refactor initial phase of transcendental solver (#5599)
commit
|
commitdiff
|
tree
2020-12-07
Andrew Reynolds
Do not expand theory definitions at the beginning of...
commit
|
commitdiff
|
tree
2020-12-07
Andrew Reynolds
(proof-new) Split proof ensure closed checks to own...
commit
|
commitdiff
|
tree
2020-12-07
Gereon Kremer
Add regression from #4927 (#5556)
commit
|
commitdiff
|
tree
2020-12-07
Andrew Reynolds
Fix bugs in getFreeVariables (#5601)
commit
|
commitdiff
|
tree
2020-12-05
Everett Maus
Change generated options to be thread_local. (#5583)
commit
|
commitdiff
|
tree
2020-12-04
Aina Niemetz
google test: expr: Migrate attribute_black. (#5598)
commit
|
commitdiff
|
tree
2020-12-04
Aina Niemetz
google test: context: Migrate cdo_black. (#5586)
commit
|
commitdiff
|
tree
2020-12-04
Aina Niemetz
google test: context: Migrate cdmap_white. (#5585)
commit
|
commitdiff
|
tree
2020-12-04
Andrew Reynolds
Fix bug in hasBoundVar (#5600)
commit
|
commitdiff
|
tree
2020-12-04
Aina Niemetz
google test: api: Migrate sort_black. (#5594)
commit
|
commitdiff
|
tree
2020-12-04
Aina Niemetz
google test: context: Migrate cdmap_black. (#5584)
commit
|
commitdiff
|
tree
2020-12-04
Aina Niemetz
google test: context: Migrate cdlist_black. (#5582)
commit
|
commitdiff
|
tree
2020-12-04
Alex Ozdemir
Use NodeDfsIterable for makeBinary (#5595)
commit
|
commitdiff
|
tree
2020-12-04
Mathias Preiner
update-copyright: Preserve file permissions. (#5597)
commit
|
commitdiff
|
tree
2020-12-03
Andrew Reynolds
(proof-new) Updates to SMT proof manager and SmtEngine...
commit
|
commitdiff
|
tree
2020-12-03
Aina Niemetz
google test: api: Migrate solver_black. (#5570)
commit
|
commitdiff
|
tree
2020-12-03
Gereon Kremer
Use mkAnd where the number of children may be less...
commit
|
commitdiff
|
tree
2020-12-03
yoni206
Models as (#5581)
commit
|
commitdiff
|
tree
2020-12-03
Aina Niemetz
google test: Add fixture for context tests. (#5590)
commit
|
commitdiff
|
tree
2020-12-03
Andrew Reynolds
Refactor handling of global declarations (#5577)
commit
|
commitdiff
|
tree
2020-12-03
Gereon Kremer
Make run_regression.py executable. (#5588)
commit
|
commitdiff
|
tree
2020-12-03
Aina Niemetz
google test: base: Migrate map_util_black. (#5580)
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
Fix RoundingMode mapping in API. (#5578)
commit
|
commitdiff
|
tree
2020-12-02
Andrew Reynolds
Remove Record object and convert to Node-level API...
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
Rename macro Message to CVC4Message. (#5576)
commit
|
commitdiff
|
tree
2020-12-02
Andrew Reynolds
Remove dagification visitor (#5574)
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
google test: api: Migrate term_black. (#5571)
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
google test: api: Use individual fixture for datatype_black...
commit
|
commitdiff
|
tree
2020-12-02
Andrew Reynolds
Add associative utilities to node manager (#5530)
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
google test: api: Migrate op_black. (#5567)
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
google test: api: Migrate grammar_black. (#5566)
commit
|
commitdiff
|
tree
2020-12-02
Andrew Reynolds
Use new let binding for cvc printer (#5561)
commit
|
commitdiff
|
tree
2020-12-02
Andrew Reynolds
(proof-new) Proofs for expand definitions (#5562)
commit
|
commitdiff
|
tree
2020-12-02
Gereon Kremer
Add regressions from #3687. (#5553)
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
google test: api: Migrate result_black. (#5569)
commit
|
commitdiff
|
tree
2020-12-02
Aina Niemetz
Remove use of this-> in FP literal. (#5565)
commit
|
commitdiff
|
tree
2020-12-02
Andrew Reynolds
Remove assertion related to CEGQI dependency lemmas...
commit
|
commitdiff
|
tree
next