projects / cvc5.git / search
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Function definition fmf preprocessing pass (#5064)
2020-09-24 Andrew Reynolds Function definition fmf preprocessing pass (#5064)
 commit | commitdiff | tree
2020-09-24 Andrew ReynoldsModify lemma vs fact policy for datatype equalities...
commit | commitdiff | tree
2020-09-23 Andrew ReynoldsDisable cegqi-bv when using sygus (#5124)
 commit | commitdiff | tree
2020-09-23 Gereon KremerMake IAND solver use inference manager. (#5126)
 commit | commitdiff | tree
2020-09-23 yoni206bv2int: new options for bvand translation (#5096)
 commit | commitdiff | tree
2020-09-23 Andrew ReynoldsAllow E-matching by default when strings are enabled...
commit | commitdiff | tree
2020-09-23 Aina NiemetzNew C++ API: Catch and throw recoverable exception...
commit | commitdiff | tree
2020-09-23 Aina NiemetzFP: Use Assert instead of AlwaysAssert in traits::...
commit | commitdiff | tree
2020-09-23 Abdalrhman MohamedRefactor Commands to use the Public API. (#5105)
 commit | commitdiff | tree
2020-09-23 Andrew ReynoldsFix type issue with term formula removal (#5107)
 commit | commitdiff | tree
2020-09-23 Andres Noetzli[Python API] Conversion to/from Unicode strings (#5120)
 commit | commitdiff | tree
2020-09-22 Aina NiemetzFP: Use Assert instead of PRECONDITION macro in converter...
commit | commitdiff | tree
2020-09-22 Mathias PreinerAdd simple BV solver (#5065)
 commit | commitdiff | tree
2020-09-22 mudathirmahgoubAdd skeleton for theory of bags (multisets) (#5100)
 commit | commitdiff | tree
2020-09-22 Andres NoetzliFix compilation without LibPoly (#5118)
 commit | commitdiff | tree
2020-09-22 makaimannAdd method to get Python object from constant value...
This PR addresses issue https://github.com/CVC4/CVC4/issues/5014. It...
commit | commitdiff | tree
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and...
commit | commitdiff | tree
2020-09-22 Gereon KremerICP-based solver for nonlinear arithmetic (#5017)
 commit | commitdiff | tree
2020-09-22 yoni206Require dumping in a dumping test (#5108)
 commit | commitdiff | tree
2020-09-21 Andrew Reynolds(proof-new) Add the arrays proof checker (#5047)
 commit | commitdiff | tree
2020-09-20 Andrew ReynoldsMore flexible design for model manager distributed...
commit | commitdiff | tree
2020-09-19 Andrew ReynoldsStandardize equality engine notifications in sets ...
commit | commitdiff | tree
2020-09-18 Andrew ReynoldsFix assertion list for globally defined recursive functions...
commit | commitdiff | tree
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 conversion...
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 statically...
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 MohamedDump 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 congruence...
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 interpolation...
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 CardinalityExtension...
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 proofs...
commit | commitdiff | tree
2020-09-04 Andrew Reynolds(new theory) Update TheoryBV to new standard for collectMode...
commit | commitdiff | tree
2020-09-04 Haniel BarbosaFix non-lib-poly-build issues (#5028)
 commit | commitdiff | tree
2020-09-04 Abdalrhman MohamedUse 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...
...for the ABC solver code base on GitHub (#4989)
 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 TheoryInferenceMana...
commit | commitdiff | tree
2020-09-03 Andrew ReynoldsUpdate sets inference manager to inherit from InferenceManag...
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
next