projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
(proof-new) SMT proof postprocess callback (#4883)
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
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-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-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-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
Andrew Reynolds
(proof-new) Witness form proof generator (#4782)
commit
|
commitdiff
|
tree
2020-08-12
Andrew Reynolds
Fix connection to master equality engine in sets (...
commit
|
commitdiff
|
tree
2020-08-12
Andrew Reynolds
Fix unsupported option in regress1. (#4874)
commit
|
commitdiff
|
tree
2020-08-12
Andrew Reynolds
Split SmtEngineState from SmtEngine (#4855)
commit
|
commitdiff
|
tree
2020-08-12
Andrew Reynolds
Prepare theory of sets for dynamic allocation of equality...
commit
|
commitdiff
|
tree
2020-08-12
Andrew Reynolds
Final preparations for changing API to use the Node...
commit
|
commitdiff
|
tree
2020-08-12
Andrew Reynolds
(proof-new) Extensions to proof checker interface ...
commit
|
commitdiff
|
tree
2020-08-11
Andrew Reynolds
Update Expr-level unit tests that depend on datatypes...
commit
|
commitdiff
|
tree
2020-08-11
Andrew Reynolds
Remove instantiation model true option (#4861)
commit
|
commitdiff
|
tree
2020-08-09
Andrew Reynolds
Make valuation class more robust to null underlying...
commit
|
commitdiff
|
tree
2020-08-09
Andrew Reynolds
Splitting a few utility classes from EqualityEngine...
commit
|
commitdiff
|
tree
2020-08-08
Andrew Reynolds
Move datatype index constant to its own file (#4859)
commit
|
commitdiff
|
tree
2020-08-06
Andrew Reynolds
Updates not related to creation for eliminating Expr...
commit
|
commitdiff
|
tree
2020-08-06
Andrew Reynolds
Split preprocessor from SmtEngine (#4854)
commit
|
commitdiff
|
tree
2020-08-06
Andrew Reynolds
(proof-new) Refactor regular expression operation ...
commit
|
commitdiff
|
tree
2020-08-05
Andrew Reynolds
Split Assertions from SmtEngine (#4788)
commit
|
commitdiff
|
tree
2020-08-04
Andrew Reynolds
Fixes for getInterpolant and getAbduct API methods...
commit
|
commitdiff
|
tree
2020-08-04
Andrew Reynolds
Add API interface for specialized constructor term...
commit
|
commitdiff
|
tree
2020-08-03
Andrew Reynolds
Generalize interface for candidate rewrite database...
commit
|
commitdiff
|
tree
2020-08-03
Andrew Reynolds
Update datatypes in cvc parser to the new API (#4826)
commit
|
commitdiff
|
tree
2020-08-03
Andrew Reynolds
Split expression names from SmtEngine (#4832)
commit
|
commitdiff
|
tree
2020-08-03
Andrew Reynolds
Split dump manager from SmtEngine (#4824)
commit
|
commitdiff
|
tree
2020-08-02
Andrew Reynolds
Updates to dtype constructor in preparation for eliminating...
commit
|
commitdiff
|
tree
2020-08-02
Andrew Reynolds
Add methods for constructing datatype types from NodeManager...
commit
|
commitdiff
|
tree
2020-08-01
Andrew Reynolds
Fix component contains for splicing due to substring...
commit
|
commitdiff
|
tree
2020-07-31
Andrew Reynolds
Split listener classes from SmtEngine (#4816)
commit
|
commitdiff
|
tree
2020-07-31
Andrew Reynolds
Standardize explanations in arrays (#4804)
commit
|
commitdiff
|
tree
2020-07-30
Andrew Reynolds
Fix null case for sygus printing (#4793)
commit
|
commitdiff
|
tree
2020-07-30
Andrew Reynolds
(proof-new) Stream output for ProofNode (#4789)
commit
|
commitdiff
|
tree
2020-07-30
Andrew Reynolds
(proof-new) Fixes for getFreeAssumptions (#4802)
commit
|
commitdiff
|
tree
2020-07-28
Andrew Reynolds
Remove arrays lazy rintro option (#4806)
commit
|
commitdiff
|
tree
2020-07-28
Andrew Reynolds
Fix regular expression delta for complement (#4765)
commit
|
commitdiff
|
tree
2020-07-28
Andrew Reynolds
Use lemma property enum for OutputChannel::lemma (...
commit
|
commitdiff
|
tree
2020-07-27
Andrew Reynolds
(proof-new) Proof production for term formula removal...
commit
|
commitdiff
|
tree
2020-07-27
Andrew Reynolds
(proof-new) Arithmetic operator elim proof producing...
commit
|
commitdiff
|
tree
2020-07-21
Andrew Reynolds
Support uninterpreted constants in the evaluator (...
commit
|
commitdiff
|
tree
2020-07-18
Andrew Reynolds
(proof-new) Proof recording for assertions pipeline...
commit
|
commitdiff
|
tree
2020-07-18
Andrew Reynolds
Enumerate shapes feature in fast sygus enumerator ...
commit
|
commitdiff
|
tree
2020-07-17
Andrew Reynolds
Replace options listener infrastructure (#4764)
commit
|
commitdiff
|
tree
2020-07-17
Andrew Reynolds
(proof-new) Updates to strings core solver (#4642)
commit
|
commitdiff
|
tree
2020-07-17
Andrew Reynolds
Add option manager and simpler option listener (#4745)
commit
|
commitdiff
|
tree
2020-07-16
Andrew Reynolds
Split abstract values utility from SmtEngine (#4754)
commit
|
commitdiff
|
tree
2020-07-16
Andrew Reynolds
Make ExtTheory a utility and not a member of Theory...
commit
|
commitdiff
|
tree
2020-07-15
Andrew Reynolds
Split abduction solver from SmtEngine (#4733)
commit
|
commitdiff
|
tree
2020-07-15
Andrew Reynolds
Simplify entailment check interface (#4744)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Make use of options in setDefaults more consistent...
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Remove sygus print callback (#4727)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Fix regression output. (#4741)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
(proof-new) Skeleton proof support in the Rewriter...
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Debug instantiations output (#4739)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Minor refactoring of subsolver initialization (#4731)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Fix type comparisons involving pointer. (#4738)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Fix whitespace issue in instantiations output. (#4737)
commit
|
commitdiff
|
tree
2020-07-13
Andrew Reynolds
(proof-new) SMT Preprocess proof generator (#4708)
commit
|
commitdiff
|
tree
2020-07-13
Andrew Reynolds
User-facing print debug option for sygus candidates...
commit
|
commitdiff
|
tree
2020-07-13
Andrew Reynolds
Statistics on instantiations per quantified formula...
commit
|
commitdiff
|
tree
2020-07-13
Andrew Reynolds
Add support for string/sequence update (#4725)
commit
|
commitdiff
|
tree
2020-07-11
Andrew Reynolds
Cache explanations in TheoryEngine::getExplanation...
commit
|
commitdiff
|
tree
2020-07-11
Andrew Reynolds
(proof-new) Add ONCE and FIXPOINT modes for term conversion...
commit
|
commitdiff
|
tree
2020-07-11
Andrew Reynolds
(proof-new) Update Theory interface for proof-new ...
commit
|
commitdiff
|
tree
2020-07-10
Andrew Reynolds
Front end support for integer AND (#4717)
commit
|
commitdiff
|
tree
2020-07-10
Andrew Reynolds
Update competition scripts (#4715)
commit
|
commitdiff
|
tree
2020-07-10
Andrew Reynolds
Ensure legal elimination for witness rewrite (#4688)
commit
|
commitdiff
|
tree
2020-07-09
Andrew Reynolds
Disable unsat cores in timeout regression (#4713)
commit
|
commitdiff
|
tree
2020-07-09
Andrew Reynolds
Associate all lemmas in non-linear arithmetic with...
commit
|
commitdiff
|
tree
2020-07-09
Andrew Reynolds
(proof-new) Theory engine proof generator (#4657)
commit
|
commitdiff
|
tree
2020-07-08
Andrew Reynolds
Always interleave theory combination with quantifiers...
commit
|
commitdiff
|
tree
2020-07-08
Andrew Reynolds
Improve and fix secant and tangent lemmas in the transcenden...
commit
|
commitdiff
|
tree
2020-07-07
Andrew Reynolds
Transfer ownership of internal Options from NodeManager...
commit
|
commitdiff
|
tree
2020-07-06
Andrew Reynolds
Front end support for sequences (#4690)
commit
|
commitdiff
|
tree
2020-07-02
Andrew Reynolds
Fix regression option (#4680)
commit
|
commitdiff
|
tree
2020-07-02
Andrew Reynolds
(proof-new) Updates to skolem manager interface (...
commit
|
commitdiff
|
tree
2020-07-02
Andrew Reynolds
(proof-new) Proof rule checkers run on skolem forms...
commit
|
commitdiff
|
tree
2020-07-02
Andrew Reynolds
(proof-new) Proof node updater (#4647)
commit
|
commitdiff
|
tree
2020-07-01
Andrew Reynolds
Add solver for integer AND (#4681)
commit
|
commitdiff
|
tree
2020-07-01
Andrew Reynolds
Inferences and model construction taking into account...
commit
|
commitdiff
|
tree
2020-07-01
Andrew Reynolds
(proof-new) Updates to evaluator (#4659)
commit
|
commitdiff
|
tree
2020-07-01
Andrew Reynolds
(proof-new) Improve rewriter for WITNESS (#4661)
commit
|
commitdiff
|
tree
2020-06-30
Andrew Reynolds
Fix normal form for re.comp (#4676)
commit
|
commitdiff
|
tree
2020-06-30
Andrew Reynolds
Simplify quantifiers strategy for when to apply last...
commit
|
commitdiff
|
tree
next