summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-09-14Merge branch 'master' into fixABCfixABCAndrew Reynolds
2020-09-14Interpolation: Add implementation for SyGuS interpolation module (final) (#5063)Ying Sheng
2020-09-14bv2int: simpler translation for plus and times (#5055)yoni206
2020-09-14Refactoring the rewriter of sets (#4856)Andrew Reynolds
2020-09-14Fix type for Windows build (#5062)Andres Noetzli
2020-09-14Standardize uses of inference manager in datatypes (#5035)Andrew Reynolds
2020-09-14Fix ABC buildAndres Noetzli
2020-09-11(proof-new) Add SMT proof manager (#5054)Andrew Reynolds
2020-09-11(proof-new) Update TheoryEngine lemma and conflict to TrustNode (#5056)Andrew Reynolds
2020-09-11Move finite model minimization to UF last call effort (#5050)Andrew Reynolds
2020-09-11(proof-new) Handle mismatched assumptions in proof equality engine during mkS...Andrew Reynolds
2020-09-11(proof-new) Use deep copy for final lemma step in proof equality engine (#5013)Andrew Reynolds
2020-09-10Add witness to cvc printer. (#5057)Andrew Reynolds
2020-09-10bv2int: refactoring the main translation loop (#5051)yoni206
2020-09-09Parser error for wrong number of datatypes (#5049)Andrew Reynolds
2020-09-09bv2int: improvement in lazy failures (#5020)yoni206
2020-09-09Use state and inference manager in UF CardinalityExtension (#5036)Andrew Reynolds
2020-09-09(proof-new) Minor changes to proof node updater (#5011)Andrew Reynolds
2020-09-09(proof-new) Make proofs in term formula removal term context sensitive (#5008)Andrew Reynolds
2020-09-09(proof-new) Generalize single step helper in eager proof generator (#5046)Andrew Reynolds
2020-09-09Fixes for regular expressions + sygus (#5044)Andrew Reynolds
2020-09-09Add is_singleton operator to the theory of sets (#5033)mudathirmahgoub
2020-09-08Split term registry from theory state in sets (#5037)Andrew Reynolds
2020-09-08Fix printing of fp values. (#5041)Mathias Preiner
2020-09-08Make CVC/API BV div/mod semantics match SMT-LIB (#4997)Andres Noetzli
2020-09-08Eliminate a custom use of TheorySep in quantifiers engine for EPR (#5039)Andrew Reynolds
2020-09-04Add asLemma flag to theory inference process (#5030)Andrew Reynolds
2020-09-04[Regressions] Fix regression issues related to BV proofs (#5029)Haniel Barbosa
2020-09-04(new theory) Update TheoryBV to new standard for collectModelValues (#5025)Andrew Reynolds
2020-09-04Fix non-lib-poly-build issues (#5028)Haniel Barbosa
2020-09-04Use Result::Sat instead of BenchmarkStatus in printers. (#5026)Abdalrhman Mohamed
2020-09-04Use arith::InferenceManager for CAD lemmas (#5015)Gereon Kremer
2020-09-04Change the unavailable ABC mercury repository for the ABC solver code base on...Malte Mues
2020-09-03Split lazy bit-vector solver from TheoryBV (#5009)Mathias Preiner
2020-09-03Add interfaces for making trust nodes in TheoryInferenceManager. (#5016)Andrew Reynolds
2020-09-03Update sets inference manager to inherit from InferenceManagerBuffered (#5007)Andrew Reynolds
2020-09-03Added a new rule to simplify (bvugt (bvurem T x) x) (#4993)Gereon Kremer
2020-09-03Minor cleanup of quantifiers engine (#4994)Andrew Reynolds
2020-09-03Changing the handled operators in bv2int preprocessing pass (#4970)yoni206
2020-09-03Basic integration of arith::InferenceManager (#4999)Gereon Kremer
2020-09-03Make nonlinear extension (more) deterministic (#4996)Gereon Kremer
2020-09-02Drop {INCLUDE,LIBRARY,RUNTIME}_INSTALL_DIR variables in CMakeLists.txt (#4979)FabianWolff
2020-09-02Make ExtTheory independent of Theory (#5010)Andrew Reynolds
2020-09-02(proof-new) Support proofs of quantifier instantiation (#5001)Andrew Reynolds
2020-09-02(proof-new) Improve debugging infrastructure for open proofs (#4984)Andrew Reynolds
2020-09-02Fix CryptoMiniSat build, regression (#5006)Andres Noetzli
2020-09-02[Python API] Add missing methods to Datatype/Term (#4998)Andres Noetzli
2020-09-02Remove #line directives from generated files. (#5005)Gereon Kremer
2020-09-02(proof-new) Updates to builtin proof checker (#4962)Andrew Reynolds
2020-09-02(proof-new) Add proof support in TheoryUF (#5002)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback