projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2020-09-18 Andrew ReynoldsAdd the shared solver (#4982) commit | commitdiff | tree
2020-09-18 yoni206bv2int: quantifiers support (#5080) commit | commitdiff | tree
2020-09-18 Andres NoetzliFix muzzled builds (#5093) commit | commitdiff | tree
2020-09-18 Haniel Barbosa[proof-new] Proof utilities for normalizing clauses... commit | commitdiff | tree
2020-09-18 Andrew ReynoldsLogic exception for arrays indexed by arrays (#5073) commit | commitdiff | tree
2020-09-18 Andres Noetzli[Strings] Fix extended equality rewriter (#5092) commit | commitdiff | tree
2020-09-18 Andrew Reynolds(proof-new) Updates to proof node updater algorithm... commit | commitdiff | tree
2020-09-18 Andrew Reynolds(proof-new) Rewrites involving operators in term conver... commit | commitdiff | tree
2020-09-17 Andrew Reynolds(proof-new) Fixes for theory engine proof generator... commit | commitdiff | tree
2020-09-17 Haniel Barbosa[proof-new] Have mkScope agnostic to True assumptions... commit | commitdiff | tree
2020-09-17 Gereon Kremer(cad-solver) Fix square-free-basis computation (#5085) commit | commitdiff | tree
2020-09-17 Andrew ReynoldsReduce recursion in term formula removal (#5052) commit | commitdiff | tree
2020-09-17 Gereon KremerUse new inference manager in transcendental solver... commit | commitdiff | tree
2020-09-17 Andrew V. JonesDo not allow to build Python bindings if building stati... commit | commitdiff | tree
2020-09-17 Andrew ReynoldsFurther standardization of datatypes (#5076) commit | commitdiff | tree
2020-09-17 yoni206Dumping internal define-funs with no arguments (#5077) commit | commitdiff | tree
2020-09-16 Andres NoetzliOnly rewrite replace_re(_all) if regexp is const (... commit | commitdiff | tree
2020-09-16 Abdalrhman... Dump commands in internal code using command printing... commit | commitdiff | tree
2020-09-16 Andrew ReynoldsAdd buffered inference manager to TheorySep (#5038) commit | commitdiff | tree
2020-09-16 Haniel Barbosa[proof-new] Adds Lazy CDProof chain data-structure... commit | commitdiff | tree
2020-09-16 Andrew ReynoldsRefactor collectModelInfo in TheoryArith (#5027) commit | commitdiff | tree
2020-09-16 yoni206bv2int: support models in tests (#5068) commit | commitdiff | tree
2020-09-16 Haniel Barbosa[proof-new] Extending eqproof conversion to HO congruen... commit | commitdiff | tree
2020-09-16 Haniel Barbosa[proof-new] Resolution rules and checkers (#5070) commit | commitdiff | tree
2020-09-16 Haniel Barbosa[proof-new] A simple proof generator for buffered proof... commit | commitdiff | tree
2020-09-16 Andrew Reynolds(proof-new) Make proofs mandatory in proof equality... commit | commitdiff | tree
2020-09-15 Andrew ReynoldsMove sets member propagation to SolverState (#5045) commit | commitdiff | tree
2020-09-15 Aina NiemetzRename system tests to api tests and remove obsolete... commit | commitdiff | tree
2020-09-15 Andrew ReynoldsMove quantifiers engine private to own file (#5053) commit | commitdiff | tree
2020-09-15 Andrew ReynoldsFix needsModel method for CEGQI (#5048) commit | commitdiff | tree
2020-09-15 Andrew ReynoldsStandard equality engine notify class for Theory (... commit | commitdiff | tree
2020-09-15 Andres NoetzliFix ABC build (#5061) commit | commitdiff | tree
2020-09-15 Ying ShengInterpolation: Add implementation for SyGuS interpolati... commit | commitdiff | tree
2020-09-14 yoni206bv2int: simpler translation for plus and times (#5055) commit | commitdiff | tree
2020-09-14 Andrew ReynoldsRefactoring the rewriter of sets (#4856) commit | commitdiff | tree
2020-09-14 Andres NoetzliFix type for Windows build (#5062) commit | commitdiff | tree
2020-09-14 Andrew ReynoldsStandardize uses of inference manager in datatypes... commit | commitdiff | tree
2020-09-12 Andrew Reynolds(proof-new) Add SMT proof manager (#5054) commit | commitdiff | tree
2020-09-12 Andrew Reynolds(proof-new) Update TheoryEngine lemma and conflict... commit | commitdiff | tree
2020-09-11 Andrew ReynoldsMove finite model minimization to UF last call effort... commit | commitdiff | tree
2020-09-11 Andrew Reynolds(proof-new) Handle mismatched assumptions in proof... commit | commitdiff | tree
2020-09-11 Andrew Reynolds(proof-new) Use deep copy for final lemma step in proof... commit | commitdiff | tree
2020-09-11 Andrew ReynoldsAdd witness to cvc printer. (#5057) commit | commitdiff | tree
2020-09-10 yoni206bv2int: refactoring the main translation loop (#5051) commit | commitdiff | tree
2020-09-10 Andrew ReynoldsParser error for wrong number of datatypes (#5049) commit | commitdiff | tree
2020-09-10 yoni206bv2int: improvement in lazy failures (#5020) commit | commitdiff | tree
2020-09-10 Andrew ReynoldsUse state and inference manager in UF CardinalityExtens... commit | commitdiff | tree
2020-09-09 Andrew Reynolds(proof-new) Minor changes to proof node updater (#5011) commit | commitdiff | tree
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
next