summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2020-09-26Use original quantified formula for single invocation reconstruction (#5129)Andrew Reynolds
2020-09-25Make sygus refinement step more robust to unevaluatable counterexamples (#5102)Andrew Reynolds
2020-09-25Cleaning and documenting cnf stream (#5134)Haniel Barbosa
2020-09-24SyGuS: Add default grammar for FP. (#5133)Aina Niemetz
2020-09-24 Function definition fmf preprocessing pass (#5064)Andrew Reynolds
2020-09-23Modify lemma vs fact policy for datatype equalities (#5115)Andrew Reynolds
2020-09-23Make IAND solver use inference manager. (#5126)Gereon Kremer
2020-09-22Allow E-matching by default when strings are enabled (#5117)Andrew Reynolds
2020-09-22FP: Use Assert instead of AlwaysAssert in traits::(pre|post)condition. (#5121)Aina Niemetz
2020-09-22FP: Use Assert instead of PRECONDITION macro in converter. (#5119)Aina Niemetz
2020-09-22Add simple BV solver (#5065)Mathias Preiner
2020-09-22Add skeleton for theory of bags (multisets) (#5100)mudathirmahgoub
2020-09-22Fix compilation without LibPoly (#5118)Andres Noetzli
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-22ICP-based solver for nonlinear arithmetic (#5017)Gereon Kremer
2020-09-21(proof-new) Add the arrays proof checker (#5047)Andrew Reynolds
2020-09-20More flexible design for model manager distributed (#4976)Andrew Reynolds
2020-09-19Standardize equality engine notifications in sets (#5098)Andrew Reynolds
2020-09-18Add the shared solver (#4982)Andrew Reynolds
2020-09-18[proof-new] Proof utilities for normalizing clauses at the Node level (#5089)Haniel Barbosa
2020-09-18Logic exception for arrays indexed by arrays (#5073)Andrew Reynolds
2020-09-18[Strings] Fix extended equality rewriter (#5092)Andres Noetzli
2020-09-17(proof-new) Fixes for theory engine proof generator (#5087)Andrew Reynolds
2020-09-17(cad-solver) Fix square-free-basis computation (#5085)Gereon Kremer
2020-09-17Use new inference manager in transcendental solver (#5022)Gereon Kremer
2020-09-16Further standardization of datatypes (#5076)Andrew Reynolds
2020-09-16Only rewrite replace_re(_all) if regexp is const (#5075)Andres Noetzli
2020-09-16Dump commands in internal code using command printing functions. (#5040)Abdalrhman Mohamed
2020-09-16Add buffered inference manager to TheorySep (#5038)Andrew Reynolds
2020-09-16Refactor collectModelInfo in TheoryArith (#5027)Andrew Reynolds
2020-09-16[proof-new] Extending eqproof conversion to HO congruence (#5071)Haniel Barbosa
2020-09-16[proof-new] Resolution rules and checkers (#5070)Haniel Barbosa
2020-09-15[proof-new] A simple proof generator for buffered proof steps (#5069)Haniel Barbosa
2020-09-15(proof-new) Make proofs mandatory in proof equality engine (#5059)Andrew Reynolds
2020-09-15Move sets member propagation to SolverState (#5045)Andrew Reynolds
2020-09-14Move quantifiers engine private to own file (#5053)Andrew Reynolds
2020-09-14Fix needsModel method for CEGQI (#5048)Andrew Reynolds
2020-09-14Standard equality engine notify class for Theory (#5042)Andrew Reynolds
2020-09-14Fix ABC build (#5061)Andres Noetzli
2020-09-14Interpolation: Add implementation for SyGuS interpolation module (final) (#5063)Ying Sheng
2020-09-14Refactoring the rewriter of sets (#4856)Andrew Reynolds
2020-09-14Standardize uses of inference manager in datatypes (#5035)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-09Use state and inference manager in UF CardinalityExtension (#5036)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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback