projects / cvc5.git / search
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
(proof-new) Updates to builtin proof checker (#4962)
2020-09-02 Andrew Reynolds(proof-new) Updates to builtin proof checker (#4962)
 commit | commitdiff | tree
2020-09-02 Andrew Reynolds(proof-new) Add proof support in TheoryUF (#5002)
 commit | commitdiff | tree
2020-09-02 Andrew Reynolds(proof-new) Make term conversion proof generator optionally...
commit | commitdiff | tree
2020-09-02 Andrew ReynoldsMinor updates to theory inference manager (#5004)
 commit | commitdiff | tree
2020-09-02 Andrew Reynolds(new theory) Update TheoryArrays to the new standard...
commit | commitdiff | tree
2020-09-02 Andrew Reynolds(new theory) Update TheorySets to the new interface...
commit | commitdiff | tree
2020-09-01 Andrew Reynolds (new theory) Update TheoryDatatypes to the new standard...
commit | commitdiff | tree
2020-09-01 Andrew ReynoldsAdd TheoryInference base class (#4990)
 commit | commitdiff | tree
2020-09-01 Andrew ReynoldsAdd the inference manager for datatypes (#4968)
 commit | commitdiff | tree
2020-08-31 Andrew Reynolds(new theory) Update TheoryStrings to new standard ...
commit | commitdiff | tree
2020-08-31 Andrew ReynoldsSimplify interface for computing relevant terms. (...
commit | commitdiff | tree
2020-08-31 Andrew ReynoldsBasic 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-28 Andrew ReynoldsReplace Theory::Set with TheoryIdSet (#4959)
 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 Andrew ReynoldsDo not delay processing equivalence class merges in...
commit | commitdiff | tree
2020-08-28 Andrew ReynoldsAdd 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-27 Andrew Reynolds(proof-new) Add the proof equality engine (#4881)
 commit | commitdiff | tree
2020-08-27 Andrew ReynoldsAdd irrelevant kinds infrastructure to TheoryModel...
commit | commitdiff | tree
2020-08-27 Andrew ReynoldsAdd 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 ReynoldsConnect combination engine to theory engine (#4940)
 commit | commitdiff | tree
2020-08-26 Andrew ReynoldsReplace Expr-level datatype with Node-level DType ...
commit | commitdiff | tree
2020-08-25 Andrew ReynoldsAdd the combination engine (#4939)
 commit | commitdiff | tree
2020-08-24 Andrew ReynoldsAdd a few basic extensions for equality engine (#4937)
 commit | commitdiff | tree
2020-08-24 Andrew ReynoldsDo not use relevance during non-linear check model...
commit | commitdiff | tree
2020-08-24 Andrew ReynoldsAdd the distributed model manager (#4934)
 commit | commitdiff | tree
2020-08-24 Andrew ReynoldsExtend the standard Theory template based on equality...
commit | commitdiff | tree
2020-08-22 Andrew ReynoldsRemove unecessary theory model builder base class ...
commit | commitdiff | tree
2020-08-21 Andrew ReynoldsDynamic allocation of model equality engine (#4911)
 commit | commitdiff | tree
2020-08-21 Andrew ReynoldsLimit trigger terms to shared terms in arrays (#4932)
 commit | commitdiff | tree
2020-08-21 Andrew ReynoldsRemove spurious theory methods calls (#4931)
 commit | commitdiff | tree
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
next