projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2020-09-09 Andrew Reynolds(proof-new) Make proofs in term formula removal term... commit | commitdiff | tree
2020-09-09 Andrew Reynolds(proof-new) Generalize single step helper in eager... commit | commitdiff | tree
2020-09-09 Andrew ReynoldsFixes for regular expressions + sygus (#5044) commit | commitdiff | tree
2020-09-09 mudathirmahgoubAdd is_singleton operator to the theory of sets (#5033) commit | commitdiff | tree
2020-09-09 Andrew ReynoldsSplit term registry from theory state in sets (#5037) commit | commitdiff | tree
2020-09-08 Mathias PreinerFix printing of fp values. (#5041) commit | commitdiff | tree
2020-09-08 Andres NoetzliMake CVC/API BV div/mod semantics match SMT-LIB (#4997) commit | commitdiff | tree
2020-09-08 Andrew ReynoldsEliminate a custom use of TheorySep in quantifiers... commit | commitdiff | tree
2020-09-04 Andrew ReynoldsAdd asLemma flag to theory inference process (#5030) commit | commitdiff | tree
2020-09-04 Haniel Barbosa[Regressions] Fix regression issues related to BV proof... commit | commitdiff | tree
2020-09-04 Andrew Reynolds(new theory) Update TheoryBV to new standard for collec... commit | commitdiff | tree
2020-09-04 Haniel BarbosaFix non-lib-poly-build issues (#5028) commit | commitdiff | tree
2020-09-04 Abdalrhman... Use Result::Sat instead of BenchmarkStatus in printers... commit | commitdiff | tree
2020-09-04 Gereon KremerUse arith::InferenceManager for CAD lemmas (#5015) commit | commitdiff | tree
2020-09-04 Malte MuesChange the unavailable ABC mercury repository for the... commit | commitdiff | tree
2020-09-04 Mathias PreinerSplit lazy bit-vector solver from TheoryBV (#5009) commit | commitdiff | tree
2020-09-04 Andrew ReynoldsAdd interfaces for making trust nodes in TheoryInferenc... commit | commitdiff | tree
2020-09-03 Andrew ReynoldsUpdate sets inference manager to inherit from Inference... commit | commitdiff | tree
2020-09-03 Gereon KremerAdded a new rule to simplify (bvugt (bvurem T x) x... commit | commitdiff | tree
2020-09-03 Andrew ReynoldsMinor cleanup of quantifiers engine (#4994) commit | commitdiff | tree
2020-09-03 yoni206Changing the handled operators in bv2int preprocessing... commit | commitdiff | tree
2020-09-03 Gereon KremerBasic integration of arith::InferenceManager (#4999) commit | commitdiff | tree
2020-09-03 Gereon KremerMake nonlinear extension (more) deterministic (#4996) commit | commitdiff | tree
2020-09-03 FabianWolffDrop {INCLUDE,LIBRARY,RUNTIME}_INSTALL_DIR variables... commit | commitdiff | tree
2020-09-03 Andrew ReynoldsMake ExtTheory independent of Theory (#5010) commit | commitdiff | tree
2020-09-03 Andrew Reynolds(proof-new) Support proofs of quantifier instantiation... commit | commitdiff | tree
2020-09-03 Andrew Reynolds(proof-new) Improve debugging infrastructure for open... commit | commitdiff | tree
2020-09-02 Andres NoetzliFix CryptoMiniSat build, regression (#5006) commit | commitdiff | tree
2020-09-02 Andres Noetzli[Python API] Add missing methods to Datatype/Term ... commit | commitdiff | tree
2020-09-02 Gereon KremerRemove #line directives from generated files. (#5005) commit | commitdiff | tree
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 Andres NoetzliUse SMT-COMP configuration for competition build (... commit | commitdiff | tree
2020-09-02 Andrew Reynolds(proof-new) Make term conversion proof generator option... commit | commitdiff | tree
2020-09-02 Andrew V. JonesMigrating from using the 'glpk-cut-log' repo to using... commit | commitdiff | tree
2020-09-02 Abdalrhman... Introduce an internal version of Commands. (#4988) 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 Gereon KremerUse std::unique_ptr instead of std::shared_ptr for... commit | commitdiff | tree
2020-09-02 Gereon KremerAdd ArithLemma and arith::InferenceManager (#4960) commit | commitdiff | tree
2020-09-02 Andrew Reynolds(new theory) Update TheorySets to the new interface... commit | commitdiff | tree
2020-09-02 Andres Noetzli[API] Fix Python Examples (#4943) commit | commitdiff | tree
2020-09-01 Haniel BarbosaRemoves old proof code (#4964) commit | commitdiff | tree
2020-09-01 Andrew Reynolds (new theory) Update TheoryDatatypes to the new standar... commit | commitdiff | tree
2020-09-01 Andrew ReynoldsAdd TheoryInference base class (#4990) commit | commitdiff | tree
2020-09-01 Aina NiemetzCMS: Update to version 5.8.0. (#4991) commit | commitdiff | tree
2020-09-01 Alex OzdemirAdd arithmetic-specific, runtime, proof-macros. (#4992) commit | commitdiff | tree
2020-09-01 FabianWolff'fix-install-headers.sh' should respect DESTDIR environ... commit | commitdiff | tree
2020-09-01 Andrew ReynoldsAdd the inference manager for datatypes (#4968) commit | commitdiff | tree
2020-09-01 FabianWolffFix spelling errors (#4977) commit | commitdiff | tree
2020-08-31 Andrew Reynolds(new theory) Update TheoryStrings to new standard ... commit | commitdiff | tree
2020-08-31 Gereon KremerFix --ackermann in the presence on syntactically differ... commit | commitdiff | tree
2020-08-31 Andrew ReynoldsSimplify interface for computing relevant terms. (... commit | commitdiff | tree
2020-08-31 Andres Noetzli[CI] Fix Cython installation (#4983) 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-29 Mathias PreinerNew C++ API: Add REGEXP_{REPEAT,LOOP}_OP handling in... commit | commitdiff | tree
2020-08-28 Andrew ReynoldsReplace Theory::Set with TheoryIdSet (#4959) commit | commitdiff | tree
2020-08-28 yoni206Incremental support for bv_to_int (#4967) 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 interf... 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 Gereon Kremer(cad-solver) Fixed excluding lemma generation. (#4958) 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-28 Gereon KremerMake iand lemmas use proper Inference types. (#4956) 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 Haniel BarbosaEliminating spurious replay of commands for define... 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 Gereon KremerFix memory issue in AntlrInput::parseError (#4873) commit | commitdiff | tree
2020-08-24 Andrew ReynoldsDo not use relevance during non-linear check model... commit | commitdiff | tree
2020-08-24 Mathias PreinerIncrease regress level to 2 for production build. ... 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 Gereon Kremer(cad solver) Add a partial check method. (#4904) commit | commitdiff | tree
2020-08-19 Andrew ReynoldsMake sets and strings solver states inherit from Theory... commit | commitdiff | tree
2020-08-19 Andres NoetzliRequire `--strings-exp` when using `str.substr` (#4916) commit | commitdiff | tree
2020-08-19 Gereon KremerChanges assertion (about maximum set cardinality) to... commit | commitdiff | tree
2020-08-19 Andres Noetzli[Regressions] Do not test `--check-proofs` anymore... commit | commitdiff | tree
2020-08-19 Gereon KremerFix SmtEngine::reset() (#4917) commit | commitdiff | tree
next