projects / cvc5.git / search
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Connect the relevance manager to TheoryEngine and use it in non-linear arithmetic...
2020-08-21 Andrew ReynoldsConnect the relevance manager to TheoryEngine and use...
commit | commitdiff | tree
2020-08-21 Andrew ReynoldsSimplify and fix care graph for ufHo (#4924)
 commit | commitdiff | tree
2020-08-21 Andrew ReynoldsRemove BV equality slicer (#4928)
 commit | commitdiff | tree
2020-08-20 Andrew ReynoldsAdd TheoryState objects to each Theory (#4920)
 commit | commitdiff | tree
2020-08-20 Andrew ReynoldsSplit QuantElimSolver from SmtEngine (#4919)
 commit | commitdiff | tree
2020-08-20 Andrew ReynoldsSimplify trigger notifications in equality engine ...
commit | commitdiff | tree
2020-08-20 Andrew ReynoldsRemove example theory (#4922)
 commit | commitdiff | tree
2020-08-20 Andrew ReynoldsAdd strings-exp to regression (#4923)
 commit | commitdiff | tree
2020-08-19 Andrew ReynoldsMake sets and strings solver states inherit from TheoryState...
commit | commitdiff | tree
2020-08-18 Andrew Reynolds(proof-new) Theory preprocessor proof producing (#4807)
 commit | commitdiff | tree
2020-08-18 Andrew ReynoldsIntroduce the theory state object (#4910)
 commit | commitdiff | tree
2020-08-18 Andrew ReynoldsStandardize 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 ReynoldsQuantifiers engine stores a pointer to the master equality...
commit | commitdiff | tree
2020-08-18 Andrew ReynoldsSplit SygusSolver from SmtEngine (#4891)
 commit | commitdiff | tree
2020-08-18 Andrew ReynoldsAdd 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 ReynoldsDynamic 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 ReynoldsAdd non-emptiness to conclusion of positive RE star...
commit | commitdiff | tree
2020-08-15 Andrew ReynoldsMinor cleanup related to notifications (#4898)
 commit | commitdiff | tree
2020-08-15 Andrew ReynoldsAdd 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 ReynoldsSimplify equality engine notifications (#4896)
 commit | commitdiff | tree
2020-08-13 Andrew ReynoldsSplit SmtSolver from SmtEngine (#4880)
 commit | commitdiff | tree
2020-08-13 Andrew ReynoldsFixes for corner case of decision tree learning with...
commit | commitdiff | tree
2020-08-13 Andrew ReynoldsMore basic fix for dumping synth-fun (#4886)
 commit | commitdiff | tree
2020-08-13 Andrew ReynoldsAdd the distributed equality engine manager (#4867)
 commit | commitdiff | tree
2020-08-12 Andrew ReynoldsFixes 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 ReynoldsFix connection to master equality engine in sets (...
commit | commitdiff | tree
2020-08-12 Andrew ReynoldsFix unsupported option in regress1. (#4874)
 commit | commitdiff | tree
2020-08-12 Andrew ReynoldsSplit SmtEngineState from SmtEngine (#4855)
 commit | commitdiff | tree
2020-08-12 Andrew ReynoldsPrepare theory of sets for dynamic allocation of equality...
commit | commitdiff | tree
2020-08-12 Andrew ReynoldsFinal 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 ReynoldsUpdate Expr-level unit tests that depend on datatypes...
commit | commitdiff | tree
2020-08-11 Andrew ReynoldsRemove instantiation model true option (#4861)
 commit | commitdiff | tree
2020-08-09 Andrew ReynoldsMake valuation class more robust to null underlying...
commit | commitdiff | tree
2020-08-09 Andrew ReynoldsSplitting a few utility classes from EqualityEngine...
commit | commitdiff | tree
2020-08-08 Andrew ReynoldsMove datatype index constant to its own file (#4859)
 commit | commitdiff | tree
2020-08-06 Andrew ReynoldsUpdates not related to creation for eliminating Expr...
commit | commitdiff | tree
2020-08-06 Andrew ReynoldsSplit 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 ReynoldsSplit Assertions from SmtEngine (#4788)
 commit | commitdiff | tree
2020-08-04 Andrew ReynoldsFixes for getInterpolant and getAbduct API methods...
commit | commitdiff | tree
2020-08-04 Andrew ReynoldsAdd API interface for specialized constructor term...
commit | commitdiff | tree
2020-08-03 Andrew ReynoldsGeneralize interface for candidate rewrite database...
commit | commitdiff | tree
2020-08-03 Andrew ReynoldsUpdate datatypes in cvc parser to the new API (#4826)
 commit | commitdiff | tree
2020-08-03 Andrew ReynoldsSplit expression names from SmtEngine (#4832)
 commit | commitdiff | tree
2020-08-03 Andrew ReynoldsSplit dump manager from SmtEngine (#4824)
 commit | commitdiff | tree
2020-08-02 Andrew ReynoldsUpdates to dtype constructor in preparation for eliminating...
commit | commitdiff | tree
2020-08-02 Andrew ReynoldsAdd methods for constructing datatype types from NodeManager...
commit | commitdiff | tree
2020-08-01 Andrew ReynoldsFix component contains for splicing due to substring...
commit | commitdiff | tree
2020-07-31 Andrew ReynoldsSplit listener classes from SmtEngine (#4816)
 commit | commitdiff | tree
2020-07-31 Andrew ReynoldsStandardize explanations in arrays (#4804)
 commit | commitdiff | tree
2020-07-30 Andrew ReynoldsFix 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 ReynoldsRemove arrays lazy rintro option (#4806)
 commit | commitdiff | tree
2020-07-28 Andrew ReynoldsFix regular expression delta for complement (#4765)
 commit | commitdiff | tree
2020-07-28 Andrew ReynoldsUse 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 ReynoldsSupport 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 ReynoldsEnumerate shapes feature in fast sygus enumerator ...
commit | commitdiff | tree
2020-07-17 Andrew ReynoldsReplace 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 ReynoldsAdd option manager and simpler option listener (#4745)
 commit | commitdiff | tree
2020-07-16 Andrew ReynoldsSplit abstract values utility from SmtEngine (#4754)
 commit | commitdiff | tree
2020-07-16 Andrew ReynoldsMake ExtTheory a utility and not a member of Theory...
commit | commitdiff | tree
2020-07-15 Andrew ReynoldsSplit abduction solver from SmtEngine (#4733)
 commit | commitdiff | tree
2020-07-15 Andrew ReynoldsSimplify entailment check interface (#4744)
 commit | commitdiff | tree
2020-07-14 Andrew ReynoldsMake use of options in setDefaults more consistent...
commit | commitdiff | tree
2020-07-14 Andrew ReynoldsRemove sygus print callback (#4727)
 commit | commitdiff | tree
2020-07-14 Andrew ReynoldsFix 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 ReynoldsDebug instantiations output (#4739)
 commit | commitdiff | tree
2020-07-14 Andrew ReynoldsMinor refactoring of subsolver initialization (#4731)
 commit | commitdiff | tree
2020-07-14 Andrew ReynoldsFix type comparisons involving pointer. (#4738)
 commit | commitdiff | tree
2020-07-14 Andrew ReynoldsFix 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 ReynoldsStatistics on instantiations per quantified formula...
commit | commitdiff | tree
2020-07-13 Andrew ReynoldsAdd support for string/sequence update (#4725)
 commit | commitdiff | tree
2020-07-11 Andrew ReynoldsCache 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 ReynoldsFront end support for integer AND (#4717)
 commit | commitdiff | tree
2020-07-10 Andrew ReynoldsUpdate competition scripts (#4715)
 commit | commitdiff | tree
2020-07-10 Andrew ReynoldsEnsure legal elimination for witness rewrite (#4688)
 commit | commitdiff | tree
2020-07-09 Andrew ReynoldsDisable unsat cores in timeout regression (#4713)
 commit | commitdiff | tree
2020-07-09 Andrew ReynoldsAssociate 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 ReynoldsAlways interleave theory combination with quantifiers...
commit | commitdiff | tree
next