projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
(proof-new) Extensions to proof checker interface (#4857)
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-11
Aina Niemetz
New C++ API: Remove redundant API functions for mkReal...
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-07
Aina Niemetz
GH Actions: Remove cancel action. (#4843)
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-05
Gereon Kremer
Improve error message for unsupported exponents (#4852)
commit
|
commitdiff
|
tree
2020-08-05
Andrew V. Jones
When checking models, ensure that error message is...
commit
|
commitdiff
|
tree
2020-08-05
Andres Noetzli
[Strings] Add eager context-dependent evaluation (...
commit
|
commitdiff
|
tree
2020-08-05
Gereon Kremer
Add dummy returns if libpoly is unavailable. (#4845)
commit
|
commitdiff
|
tree
2020-08-04
Andrew Reynolds
Fixes for getInterpolant and getAbduct API methods...
commit
|
commitdiff
|
tree
2020-08-04
Mathias Preiner
Add documentation and build instructions for recompilation...
commit
|
commitdiff
|
tree
2020-08-04
Abdalrhman Mohamed
Modify the smt2 parser to use the Sygus grammar. (...
commit
|
commitdiff
|
tree
2020-08-04
Andrew Reynolds
Add API interface for specialized constructor term...
commit
|
commitdiff
|
tree
2020-08-04
Gereon Kremer
Properly initialize d_fullyInited. (#4840)
commit
|
commitdiff
|
tree
2020-08-04
Gereon Kremer
Add CAD-based solver (#4834)
commit
|
commitdiff
|
tree
2020-08-03
Andres Noetzli
Update documentation for Solver::mkVar() (#4833)
commit
|
commitdiff
|
tree
2020-08-03
Ying Sheng
Add implementation for SyGuS interpolation module ...
commit
|
commitdiff
|
tree
2020-08-03
yoni206
New BV rewrite rules aimed at bv_to_int preprocessing...
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
yoni206
Examples for using sygus python api (#4822)
commit
|
commitdiff
|
tree
2020-08-03
makaimann
Delete solver pointer in Cython __dealloc__ (#4799)
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
Andres Noetzli
Fix ASan failure in interactive_shell_black (#4827)
commit
|
commitdiff
|
tree
2020-08-02
Andres Noetzli
Ensure strict length constraint for decompose rule...
commit
|
commitdiff
|
tree
2020-08-02
Andrew Reynolds
Add methods for constructing datatype types from NodeManager...
commit
|
commitdiff
|
tree
2020-08-01
Andrew V. Jones
Ensure that we only find '.a's when building statically...
commit
|
commitdiff
|
tree
2020-08-01
Andrew Reynolds
Fix component contains for splicing due to substring...
commit
|
commitdiff
|
tree
2020-08-01
yoni206
Add SyGuS Python API (#4812)
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
Andres Noetzli
Python API: Add support for sequences (#4757)
commit
|
commitdiff
|
tree
2020-07-30
Gereon Kremer
Cad implementation (#4774)
commit
|
commitdiff
|
tree
2020-07-30
Gereon Kremer
Adds the interface for the CAD-based arithmetic solver...
commit
|
commitdiff
|
tree
2020-07-30
Andrew V. Jones
When linking Editline, use 'pkg-config' to correctly...
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
Ying Sheng
fixing issue #4808. (#4810)
commit
|
commitdiff
|
tree
2020-07-28
Andrew Reynolds
Remove arrays lazy rintro option (#4806)
commit
|
commitdiff
|
tree
2020-07-28
Andres Noetzli
Replace Expr with Node in Term/Op (#4781)
commit
|
commitdiff
|
tree
2020-07-28
Andrew Reynolds
Fix regular expression delta for complement (#4765)
commit
|
commitdiff
|
tree
2020-07-28
yoni206
Supporting seq.nth (#4723)
commit
|
commitdiff
|
tree
2020-07-28
Ying Sheng
Interpolation: Add interface for SyGuS interpolation...
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-27
Alex Ozdemir
Consider negation's proof before triggering arith pfs...
commit
|
commitdiff
|
tree
2020-07-21
Aina Niemetz
GH Actions: Cancel builds on push, remove redundant...
commit
|
commitdiff
|
tree
2020-07-21
Andrew Reynolds
Support uninterpreted constants in the evaluator (...
commit
|
commitdiff
|
tree
2020-07-21
Gereon Kremer
Preparations for a CAD-based arithmetic solver (#4762)
commit
|
commitdiff
|
tree
2020-07-20
Alex Ozdemir
Fix a deadlock in the signature tests. (#4772)
...a duplicate of [this](https://
github
.com/CVC4/LFSC/pull/38).
commit
|
commitdiff
|
tree
2020-07-18
Haniel Barbosa
Improving equality engine tracing (#4770)
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
Andres Noetzli
Add NodeManagerScopes to fix use-after-free issues...
commit
|
commitdiff
|
tree
2020-07-17
Andrew Reynolds
Replace options listener infrastructure (#4764)
commit
|
commitdiff
|
tree
2020-07-17
Andrew V. Jones
Support for using 'libedit' over 'readline' #4571 ...
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-17
Gereon Kremer
Integration of libpoly (#4679)
commit
|
commitdiff
|
tree
2020-07-17
Haniel Barbosa
Fix EqProof to ProofNode conversion (#4760)
commit
|
commitdiff
|
tree
2020-07-16
Haniel Barbosa
(proof-new) Implements the conversion between EqProof...
commit
|
commitdiff
|
tree
2020-07-16
Gereon Kremer
Resource manager cleanup (#4732)
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-16
Gereon Kremer
Remove cumulative time limits and cpu time limits ...
commit
|
commitdiff
|
tree
2020-07-16
Gereon Kremer
Fixes memory leak when an exception goes through runCvc4...
commit
|
commitdiff
|
tree
2020-07-16
Haniel Barbosa
(proof-new) Adding API for converting EqProof into...
commit
|
commitdiff
|
tree
2020-07-15
Andres Noetzli
Use Nodes for SmtEngine assertions (#4752)
commit
|
commitdiff
|
tree
2020-07-15
Andrew Reynolds
Split abduction solver from SmtEngine (#4733)
commit
|
commitdiff
|
tree
2020-07-15
Andres Noetzli
Use TypeNode in UninterpretedConstant (#4748)
commit
|
commitdiff
|
tree
2020-07-15
Gereon Kremer
Add missing header (Fixes #4743) (#4749)
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
Andres Noetzli
Use TypeNode in EmptySet (#4740)
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
Andres Noetzli
Fix caching in TheoryEngine::getExplanation() (#4736)
commit
|
commitdiff
|
tree
2020-07-14
Haniel Barbosa
Fix options messages that were inverted (#4734)
commit
|
commitdiff
|
tree
2020-07-14
Andres Noetzli
Use TypeNode/Node in ArrayStoreAll (#4728)
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
Gereon Kremer
Implement --tlimit for windows (#4716)
commit
|
commitdiff
|
tree
2020-07-13
Andrew Reynolds
Add support for string/sequence update (#4725)
commit
|
commitdiff
|
tree
next