projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Use std::unique_ptr instead of std::shared_ptr for inference manager (#5003)
2020-09-02
Gereon Kremer
Use std::unique_ptr instead of std::shared_ptr for...
commit
|
commitdiff
|
tree
2020-09-02
Gereon Kremer
Add ArithLemma and arith::InferenceManager (#4960)
commit
|
commitdiff
|
tree
2020-09-02
Andrew Reynolds
(new theory) Update TheorySets to the new interface...
commit
|
commitdiff
|
tree
2020-09-02
Andres Noetzli
[API] Fix Python Examples (#4943)
commit
|
commitdiff
|
tree
2020-09-01
Haniel Barbosa
Removes old proof code (#4964)
commit
|
commitdiff
|
tree
2020-09-01
Andrew Reynolds
(new theory) Update TheoryDatatypes to the new standard...
commit
|
commitdiff
|
tree
2020-09-01
Andrew Reynolds
Add TheoryInference base class (#4990)
commit
|
commitdiff
|
tree
2020-09-01
Aina Niemetz
CMS: Update to version 5.8.0. (#4991)
commit
|
commitdiff
|
tree
2020-09-01
Alex Ozdemir
Add arithmetic-specific, runtime, proof-macros. (#4992)
commit
|
commitdiff
|
tree
2020-09-01
FabianWolff
'fix-install-headers.sh' should respect DESTDIR environment...
commit
|
commitdiff
|
tree
2020-09-01
Andrew Reynolds
Add the inference manager for datatypes (#4968)
commit
|
commitdiff
|
tree
2020-09-01
FabianWolff
Fix spelling errors (#4977)
commit
|
commitdiff
|
tree
2020-08-31
Andrew Reynolds
(new theory) Update TheoryStrings to new standard ...
commit
|
commitdiff
|
tree
2020-08-31
Gereon Kremer
Fix --ackermann in the presence on syntactically different...
commit
|
commitdiff
|
tree
2020-08-31
Andrew Reynolds
Simplify interface for computing relevant terms. (...
commit
|
commitdiff
|
tree
2020-08-31
Andres Noetzli
[CI] Fix Cython installation (#4983)
commit
|
commitdiff
|
tree
2020-08-31
Andrew Reynolds
Basic proof support in inference manager (#4975)
commit
|
commitdiff
|
tree
2020-08-29
Andrew Reynolds
(proof-new) More term context utilities. (#4912)
commit
|
commitdiff
|
tree
2020-08-29
Mathias Preiner
New C++ API: Add REGEXP_{REPEAT,LOOP}_OP handling in...
commit
|
commitdiff
|
tree
2020-08-28
Andrew Reynolds
Replace Theory::Set with TheoryIdSet (#4959)
commit
|
commitdiff
|
tree
2020-08-28
yoni206
Incremental support for bv_to_int (#4967)
commit
|
commitdiff
|
tree
2020-08-28
Andrew Reynolds
(proof-new) Make CombinationEngine proof producing...
commit
|
commitdiff
|
tree
2020-08-28
Andrew Reynolds
(new theory) Update TheoryQuantifiers to the new interface...
commit
|
commitdiff
|
tree
2020-08-28
Andrew Reynolds
(proof-new) Add the SMT proof post processor (#4913)
commit
|
commitdiff
|
tree
2020-08-28
Andrew Reynolds
(new theory) Update TheoryFP to the new interface ...
commit
|
commitdiff
|
tree
2020-08-28
Gereon Kremer
(cad-solver) Fixed excluding lemma generation. (#4958)
commit
|
commitdiff
|
tree
2020-08-28
Andrew Reynolds
Do not delay processing equivalence class merges in...
commit
|
commitdiff
|
tree
2020-08-28
Andrew Reynolds
Add the buffered inference manager (#4954)
commit
|
commitdiff
|
tree
2020-08-28
Andrew Reynolds
(new theory) Update TheorySep to new interface (#4947)
commit
|
commitdiff
|
tree
2020-08-28
Gereon Kremer
Make iand lemmas use proper Inference types. (#4956)
commit
|
commitdiff
|
tree
2020-08-27
Andrew Reynolds
(proof-new) Add the proof equality engine (#4881)
commit
|
commitdiff
|
tree
2020-08-27
Andrew Reynolds
Add irrelevant kinds infrastructure to TheoryModel...
commit
|
commitdiff
|
tree
2020-08-27
Andrew Reynolds
Add the theory inference manager (#4948)
commit
|
commitdiff
|
tree
2020-08-27
Andrew Reynolds
(new theory) Update TheoryUF to new interface (#4944)
commit
|
commitdiff
|
tree
2020-08-26
Andrew Reynolds
Connect combination engine to theory engine (#4940)
commit
|
commitdiff
|
tree
2020-08-26
Andrew Reynolds
Replace Expr-level datatype with Node-level DType ...
commit
|
commitdiff
|
tree
2020-08-25
Haniel Barbosa
Eliminating spurious replay of commands for define...
commit
|
commitdiff
|
tree
2020-08-25
Andrew Reynolds
Add the combination engine (#4939)
commit
|
commitdiff
|
tree
2020-08-24
Andrew Reynolds
Add a few basic extensions for equality engine (#4937)
commit
|
commitdiff
|
tree
2020-08-24
Gereon Kremer
Fix memory issue in AntlrInput::parseError (#4873)
commit
|
commitdiff
|
tree
2020-08-24
Andrew Reynolds
Do not use relevance during non-linear check model...
commit
|
commitdiff
|
tree
2020-08-24
Mathias Preiner
Increase regress level to 2 for production build. ...
commit
|
commitdiff
|
tree
2020-08-24
Andrew Reynolds
Add the distributed model manager (#4934)
commit
|
commitdiff
|
tree
2020-08-24
Andrew Reynolds
Extend the standard Theory template based on equality...
commit
|
commitdiff
|
tree
2020-08-22
Andrew Reynolds
Remove unecessary theory model builder base class ...
commit
|
commitdiff
|
tree
2020-08-21
Andrew Reynolds
Dynamic allocation of model equality engine (#4911)
commit
|
commitdiff
|
tree
2020-08-21
Andrew Reynolds
Limit trigger terms to shared terms in arrays (#4932)
commit
|
commitdiff
|
tree
2020-08-21
Andrew Reynolds
Remove spurious theory methods calls (#4931)
commit
|
commitdiff
|
tree
2020-08-21
Andrew Reynolds
Connect the relevance manager to TheoryEngine and use...
commit
|
commitdiff
|
tree
2020-08-21
Andrew Reynolds
Simplify and fix care graph for ufHo (#4924)
commit
|
commitdiff
|
tree
2020-08-21
Andrew Reynolds
Remove BV equality slicer (#4928)
commit
|
commitdiff
|
tree
2020-08-20
Andrew Reynolds
Add TheoryState objects to each Theory (#4920)
commit
|
commitdiff
|
tree
2020-08-20
Andrew Reynolds
Split QuantElimSolver from SmtEngine (#4919)
commit
|
commitdiff
|
tree
2020-08-20
Andrew Reynolds
Simplify trigger notifications in equality engine ...
commit
|
commitdiff
|
tree
2020-08-20
Andrew Reynolds
Remove example theory (#4922)
commit
|
commitdiff
|
tree
2020-08-20
Andrew Reynolds
Add strings-exp to regression (#4923)
commit
|
commitdiff
|
tree
2020-08-19
Gereon Kremer
(cad solver) Add a partial check method. (#4904)
commit
|
commitdiff
|
tree
2020-08-19
Andrew Reynolds
Make sets and strings solver states inherit from TheoryState...
commit
|
commitdiff
|
tree
2020-08-19
Andres Noetzli
Require `--strings-exp` when using `str.substr` (#4916)
commit
|
commitdiff
|
tree
2020-08-19
Gereon Kremer
Changes assertion (about maximum set cardinality) to...
commit
|
commitdiff
|
tree
2020-08-19
Andres Noetzli
[Regressions] Do not test `--check-proofs` anymore...
commit
|
commitdiff
|
tree
2020-08-19
Gereon Kremer
Fix SmtEngine::reset() (#4917)
commit
|
commitdiff
|
tree
2020-08-18
Abdalrhman Mohamed
Refactor functions that print commands (Part 2) (#4905)
commit
|
commitdiff
|
tree
2020-08-18
Andrew Reynolds
(proof-new) Theory preprocessor proof producing (#4807)
commit
|
commitdiff
|
tree
2020-08-18
Andrew Reynolds
Introduce the theory state object (#4910)
commit
|
commitdiff
|
tree
2020-08-18
Andrew Reynolds
Standardize collectModelInfo and theory-specific collectRele...
commit
|
commitdiff
|
tree
2020-08-18
Andrew Reynolds
(proof-new) Minor updates to trust node (#4900)
commit
|
commitdiff
|
tree
2020-08-18
Andrew Reynolds
(proof-new) SMT proof postprocess callback (#4883)
commit
|
commitdiff
|
tree
2020-08-18
Andrew Reynolds
Quantifiers engine stores a pointer to the master equality...
commit
|
commitdiff
|
tree
2020-08-18
Andrew Reynolds
Split SygusSolver from SmtEngine (#4891)
commit
|
commitdiff
|
tree
2020-08-18
Andrew Reynolds
Add the relevance manager module (#4894)
commit
|
commitdiff
|
tree
2020-08-18
Andrew Reynolds
(proof-new) Callbacks for term-context-sensitive terms...
commit
|
commitdiff
|
tree
2020-08-17
Alex Ozdemir
Add identifier name for side condition. (#4902)
commit
|
commitdiff
|
tree
2020-08-17
Andres Noetzli
[CI] Update package list (#4906)
commit
|
commitdiff
|
tree
2020-08-17
Andrew Reynolds
Dynamic allocation of equality engine in Theory (#4890)
commit
|
commitdiff
|
tree
2020-08-17
Andrew Reynolds
(proof-new) Prepare the theory of strings for proof...
commit
|
commitdiff
|
tree
2020-08-16
Andrew Reynolds
Add non-emptiness to conclusion of positive RE star...
commit
|
commitdiff
|
tree
2020-08-16
Gereon Kremer
(cad solver) Use the current model as initial assignment...
commit
|
commitdiff
|
tree
2020-08-15
Andrew Reynolds
Minor cleanup related to notifications (#4898)
commit
|
commitdiff
|
tree
2020-08-15
Andrew Reynolds
Add finishInit method to PropEngine (#4895)
commit
|
commitdiff
|
tree
2020-08-15
Andrew Reynolds
(proof-new) Add the strings proof checker (#4858)
commit
|
commitdiff
|
tree
2020-08-14
Andrew Reynolds
Simplify equality engine notifications (#4896)
commit
|
commitdiff
|
tree
2020-08-14
E Polgreen
correctly parse sygus lang option (#4884)
commit
|
commitdiff
|
tree
2020-08-14
Gereon Kremer
Inspect roots to avoid certain resultants (Algorithm...
commit
|
commitdiff
|
tree
2020-08-13
Andrew Reynolds
Split SmtSolver from SmtEngine (#4880)
commit
|
commitdiff
|
tree
2020-08-13
Andrew Reynolds
Fixes for corner case of decision tree learning with...
commit
|
commitdiff
|
tree
2020-08-13
Andrew Reynolds
More basic fix for dumping synth-fun (#4886)
commit
|
commitdiff
|
tree
2020-08-13
Andrew Reynolds
Add the distributed equality engine manager (#4867)
commit
|
commitdiff
|
tree
2020-08-13
Haniel Barbosa
[proof-new] Adding support for corner case of transitivity...
commit
|
commitdiff
|
tree
2020-08-12
Haniel Barbosa
generalize handling MERGED_THROUGH_CONSTANST in EqProof...
commit
|
commitdiff
|
tree
2020-08-12
Abdalrhman Mohamed
Refactor functions that print commands (Part 1) (#4869)
commit
|
commitdiff
|
tree
2020-08-12
Andrew Reynolds
Fixes for degenerate case of sygus decision tree learning...
commit
|
commitdiff
|
tree
2020-08-12
Andrew Reynolds
(proof-new) Improve robustness of CONG rule (#4882)
commit
|
commitdiff
|
tree
2020-08-12
Andrew Reynolds
(proof-new) Proof support in the strings term registry...
commit
|
commitdiff
|
tree
2020-08-12
Andrew Reynolds
(proof-new) Improve interfaces to proof generators...
commit
|
commitdiff
|
tree
2020-08-12
makaimann
Add option to only build library (#4801)
commit
|
commitdiff
|
tree
2020-08-12
Andrew Reynolds
(proof-new) Witness form proof generator (#4782)
commit
|
commitdiff
|
tree
2020-08-12
Gereon Kremer
Add naive support for integer variables. (#4835)
commit
|
commitdiff
|
tree
2020-08-12
Haniel Barbosa
(proof-new) Improving proof-production in Equality...
commit
|
commitdiff
|
tree
2020-08-12
Andrew Reynolds
Fix connection to master equality engine in sets (...
commit
|
commitdiff
|
tree
next