projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Standardize collectModelInfo and theory-specific collectRelevantTerms (#4909)
[cvc5.git]
/
src
/
2020-08-18
Andrew Reynolds
Standardize collectModelInfo and theory-specific collec...
tree
|
commitdiff
2020-08-18
Andrew Reynolds
(proof-new) Minor updates to trust node (#4900)
tree
|
commitdiff
2020-08-18
Andrew Reynolds
(proof-new) SMT proof postprocess callback (#4883)
tree
|
commitdiff
2020-08-18
Andrew Reynolds
Quantifiers engine stores a pointer to the master equal...
tree
|
commitdiff
2020-08-18
Andrew Reynolds
Split SygusSolver from SmtEngine (#4891)
tree
|
commitdiff
2020-08-18
Andrew Reynolds
Add the relevance manager module (#4894)
tree
|
commitdiff
2020-08-18
Andrew Reynolds
(proof-new) Callbacks for term-context-sensitive terms...
tree
|
commitdiff
2020-08-17
Andrew Reynolds
Dynamic allocation of equality engine in Theory (#4890)
tree
|
commitdiff
2020-08-17
Andrew Reynolds
(proof-new) Prepare the theory of strings for proof...
tree
|
commitdiff
2020-08-16
Andrew Reynolds
Add non-emptiness to conclusion of positive RE star...
tree
|
commitdiff
2020-08-16
Gereon Kremer
(cad solver) Use the current model as initial assignmen...
tree
|
commitdiff
2020-08-15
Andrew Reynolds
Minor cleanup related to notifications (#4898)
tree
|
commitdiff
2020-08-15
Andrew Reynolds
Add finishInit method to PropEngine (#4895)
tree
|
commitdiff
2020-08-15
Andrew Reynolds
(proof-new) Add the strings proof checker (#4858)
tree
|
commitdiff
2020-08-14
Andrew Reynolds
Simplify equality engine notifications (#4896)
tree
|
commitdiff
2020-08-14
E Polgreen
correctly parse sygus lang option (#4884)
tree
|
commitdiff
2020-08-14
Gereon Kremer
Inspect roots to avoid certain resultants (Algorithm...
tree
|
commitdiff
2020-08-13
Andrew Reynolds
Split SmtSolver from SmtEngine (#4880)
tree
|
commitdiff
2020-08-13
Andrew Reynolds
Fixes for corner case of decision tree learning with...
tree
|
commitdiff
2020-08-13
Andrew Reynolds
More basic fix for dumping synth-fun (#4886)
tree
|
commitdiff
2020-08-13
Andrew Reynolds
Add the distributed equality engine manager (#4867)
tree
|
commitdiff
2020-08-13
Haniel Barbosa
[proof-new] Adding support for corner case of transitiv...
tree
|
commitdiff
2020-08-12
Haniel Barbosa
generalize handling MERGED_THROUGH_CONSTANST in EqProof...
tree
|
commitdiff
2020-08-12
Abdalrhman Mohamed
Refactor functions that print commands (Part 1) (#4869)
tree
|
commitdiff
2020-08-12
Andrew Reynolds
Fixes for degenerate case of sygus decision tree learni...
tree
|
commitdiff
2020-08-12
Andrew Reynolds
(proof-new) Improve robustness of CONG rule (#4882)
tree
|
commitdiff
2020-08-12
Andrew Reynolds
(proof-new) Proof support in the strings term registry...
tree
|
commitdiff
2020-08-12
Andrew Reynolds
(proof-new) Improve interfaces to proof generators...
tree
|
commitdiff
2020-08-12
makaimann
Add option to only build library (#4801)
tree
|
commitdiff
2020-08-12
Andrew Reynolds
(proof-new) Witness form proof generator (#4782)
tree
|
commitdiff
2020-08-12
Gereon Kremer
Add naive support for integer variables. (#4835)
tree
|
commitdiff
2020-08-12
Haniel Barbosa
(proof-new) Improving proof-production in Equality...
tree
|
commitdiff
2020-08-12
Andrew Reynolds
Fix connection to master equality engine in sets (...
tree
|
commitdiff
2020-08-12
Gereon Kremer
Fix infinite loop in arith_ite_simp (#4805)
tree
|
commitdiff
2020-08-12
Andrew Reynolds
Split SmtEngineState from SmtEngine (#4855)
tree
|
commitdiff
2020-08-12
Andrew Reynolds
Prepare theory of sets for dynamic allocation of equali...
tree
|
commitdiff
2020-08-12
Andrew Reynolds
Final preparations for changing API to use the Node...
tree
|
commitdiff
2020-08-12
Andrew Reynolds
(proof-new) Extensions to proof checker interface ...
tree
|
commitdiff
2020-08-11
Andrew Reynolds
Remove instantiation model true option (#4861)
tree
|
commitdiff
2020-08-11
Aina Niemetz
New C++ API: Remove redundant API functions for mkReal...
tree
|
commitdiff
2020-08-09
Andrew Reynolds
Make valuation class more robust to null underlying...
tree
|
commitdiff
2020-08-09
Andrew Reynolds
Splitting a few utility classes from EqualityEngine...
tree
|
commitdiff
2020-08-08
Andrew Reynolds
Move datatype index constant to its own file (#4859)
tree
|
commitdiff
2020-08-06
Andrew Reynolds
Updates not related to creation for eliminating Expr...
tree
|
commitdiff
2020-08-06
Andrew Reynolds
Split preprocessor from SmtEngine (#4854)
tree
|
commitdiff
2020-08-06
Andrew Reynolds
(proof-new) Refactor regular expression operation ...
tree
|
commitdiff
2020-08-05
Andrew Reynolds
Split Assertions from SmtEngine (#4788)
tree
|
commitdiff
2020-08-05
Gereon Kremer
Improve error message for unsupported exponents (#4852)
tree
|
commitdiff
2020-08-05
Andrew V. Jones
When checking models, ensure that error message is...
tree
|
commitdiff
2020-08-05
Andres Noetzli
[Strings] Add eager context-dependent evaluation (...
tree
|
commitdiff
2020-08-05
Gereon Kremer
Add dummy returns if libpoly is unavailable. (#4845)
tree
|
commitdiff
2020-08-04
Andrew Reynolds
Fixes for getInterpolant and getAbduct API methods...
tree
|
commitdiff
2020-08-04
Mathias Preiner
Add documentation and build instructions for recompilat...
tree
|
commitdiff
2020-08-04
Abdalrhman Mohamed
Modify the smt2 parser to use the Sygus grammar. (...
tree
|
commitdiff
2020-08-04
Andrew Reynolds
Add API interface for specialized constructor term...
tree
|
commitdiff
2020-08-04
Gereon Kremer
Properly initialize d_fullyInited. (#4840)
tree
|
commitdiff
2020-08-04
Gereon Kremer
Add CAD-based solver (#4834)
tree
|
commitdiff
2020-08-03
Andres Noetzli
Update documentation for Solver::mkVar() (#4833)
tree
|
commitdiff
2020-08-03
Ying Sheng
Add implementation for SyGuS interpolation module ...
tree
|
commitdiff
2020-08-03
yoni206
New BV rewrite rules aimed at bv_to_int preprocessing...
tree
|
commitdiff
2020-08-03
Andrew Reynolds
Generalize interface for candidate rewrite database...
tree
|
commitdiff
2020-08-03
Andrew Reynolds
Update datatypes in cvc parser to the new API (#4826)
tree
|
commitdiff
2020-08-03
makaimann
Delete solver pointer in Cython __dealloc__ (#4799)
tree
|
commitdiff
2020-08-03
Andrew Reynolds
Split expression names from SmtEngine (#4832)
tree
|
commitdiff
2020-08-03
Andrew Reynolds
Split dump manager from SmtEngine (#4824)
tree
|
commitdiff
2020-08-02
Andrew Reynolds
Updates to dtype constructor in preparation for elimina...
tree
|
commitdiff
2020-08-02
Andres Noetzli
Fix ASan failure in interactive_shell_black (#4827)
tree
|
commitdiff
2020-08-02
Andres Noetzli
Ensure strict length constraint for decompose rule...
tree
|
commitdiff
2020-08-02
Andrew Reynolds
Add methods for constructing datatype types from NodeMa...
tree
|
commitdiff
2020-08-01
Andrew Reynolds
Fix component contains for splicing due to substring...
tree
|
commitdiff
2020-08-01
yoni206
Add SyGuS Python API (#4812)
tree
|
commitdiff
2020-07-31
Andrew Reynolds
Split listener classes from SmtEngine (#4816)
tree
|
commitdiff
2020-07-31
Andrew Reynolds
Standardize explanations in arrays (#4804)
tree
|
commitdiff
2020-07-30
Andres Noetzli
Python API: Add support for sequences (#4757)
tree
|
commitdiff
2020-07-30
Gereon Kremer
Cad implementation (#4774)
tree
|
commitdiff
2020-07-30
Gereon Kremer
Adds the interface for the CAD-based arithmetic solver...
tree
|
commitdiff
2020-07-30
Andrew V. Jones
When linking Editline, use 'pkg-config' to correctly...
tree
|
commitdiff
2020-07-30
Andrew Reynolds
Fix null case for sygus printing (#4793)
tree
|
commitdiff
2020-07-30
Andrew Reynolds
(proof-new) Stream output for ProofNode (#4789)
tree
|
commitdiff
2020-07-30
Andrew Reynolds
(proof-new) Fixes for getFreeAssumptions (#4802)
tree
|
commitdiff
2020-07-28
Ying Sheng
fixing issue #4808. (#4810)
tree
|
commitdiff
2020-07-28
Andrew Reynolds
Remove arrays lazy rintro option (#4806)
tree
|
commitdiff
2020-07-28
Andres Noetzli
Replace Expr with Node in Term/Op (#4781)
tree
|
commitdiff
2020-07-28
Andrew Reynolds
Fix regular expression delta for complement (#4765)
tree
|
commitdiff
2020-07-28
yoni206
Supporting seq.nth (#4723)
tree
|
commitdiff
2020-07-28
Ying Sheng
Interpolation: Add interface for SyGuS interpolation...
tree
|
commitdiff
2020-07-28
Andrew Reynolds
Use lemma property enum for OutputChannel::lemma (...
tree
|
commitdiff
2020-07-27
Andrew Reynolds
(proof-new) Proof production for term formula removal...
tree
|
commitdiff
2020-07-27
Andrew Reynolds
(proof-new) Arithmetic operator elim proof producing...
tree
|
commitdiff
2020-07-27
Alex Ozdemir
Consider negation's proof before triggering arith pfs...
tree
|
commitdiff
2020-07-21
Andrew Reynolds
Support uninterpreted constants in the evaluator (...
tree
|
commitdiff
2020-07-21
Gereon Kremer
Preparations for a CAD-based arithmetic solver (#4762)
tree
|
commitdiff
2020-07-18
Haniel Barbosa
Improving equality engine tracing (#4770)
tree
|
commitdiff
2020-07-18
Andrew Reynolds
(proof-new) Proof recording for assertions pipeline...
tree
|
commitdiff
2020-07-18
Andrew Reynolds
Enumerate shapes feature in fast sygus enumerator ...
tree
|
commitdiff
2020-07-17
Andres Noetzli
Add NodeManagerScopes to fix use-after-free issues...
tree
|
commitdiff
2020-07-17
Andrew Reynolds
Replace options listener infrastructure (#4764)
tree
|
commitdiff
2020-07-17
Andrew V. Jones
Support for using 'libedit' over 'readline' #4571 ...
tree
|
commitdiff
2020-07-17
Andrew Reynolds
(proof-new) Updates to strings core solver (#4642)
tree
|
commitdiff
2020-07-17
Andrew Reynolds
Add option manager and simpler option listener (#4745)
tree
|
commitdiff
next