projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Make sure conflicts are not rewritten (in arithmetic) (#5219)
[cvc5.git] / src /
2020-10-07 Gereon KremerMake sure conflicts are not rewritten (in arithmetic... tree | commitdiff
2020-10-07 Andrew Reynolds(proof-new) Add the strings proof constructor (#4903) tree | commitdiff
2020-10-07 Andrew ReynoldsProcess pending inferences at the beginning of datatype... tree | commitdiff
2020-10-06 yoni206bv-to-int: change order of passes (#5208) tree | commitdiff
2020-10-06 Alex Ozdemir(proof-new) proofs for ArithCongMan -> ee facts (#5207) tree | commitdiff
2020-10-06 Andrew Reynolds(proof-new) Add interface for trusted substitution... tree | commitdiff
2020-10-06 Andrew Reynolds(proof-new) Allow null proofs from generators in LazyCD... tree | commitdiff
2020-10-06 mudathirmahgoubAdd operators bag.from_set, bag.to_set to the theory... tree | commitdiff
2020-10-06 Andrew ReynoldsAdd arithmetic preprocess module (#5188) tree | commitdiff
2020-10-06 Abdalrhman MohamedRecover from some exceptions. (#5203) tree | commitdiff
2020-10-06 mudathirmahgoubRemove subtyping for sets (#5205) tree | commitdiff
2020-10-05 Aina NiemetzSyGuS: Add fp.sub to default FP grammar. (#5206) tree | commitdiff
2020-10-05 Aina NiemetzInteger: GMP: Move implementation of member functions... tree | commitdiff
2020-10-05 Andrew ReynoldsMake sygus more robust to unknown responses in solution... tree | commitdiff
2020-10-04 mudathirmahgoubRemove subtyping for sets theory (#5179) tree | commitdiff
2020-10-03 Aina Niemetzsygus-inst: Add more special BV values. (#5191) tree | commitdiff
2020-10-03 Andrew ReynoldsStandardization of Theory (#5181) tree | commitdiff
2020-10-02 Andrew ReynoldsMinor simplifications to substitution map class (#5180) tree | commitdiff
2020-10-02 Andrew Reynolds(proof-new) Fixes for theory preprocessing proofs ... tree | commitdiff
2020-10-02 Andrew Reynolds(proof-new) Make shared solver proof producing (#5169) tree | commitdiff
2020-10-02 Gereon KremerAllow for theory combination of strings with nonlinear... tree | commitdiff
2020-10-02 Andrew ReynoldsDecouple modules from TheoryArithPrivate (#5184) tree | commitdiff
2020-10-02 Alex Ozdemir(proof-new) New proofs in arith::Constraint::externalEx... tree | commitdiff
2020-10-02 Aina NiemetzSyGuS: Add min/max (sub)normal constants to FP default... tree | commitdiff
2020-10-01 Andrew Reynolds(proof-new) Make arrays proof producing (#5112) tree | commitdiff
2020-10-01 Mathias PreinerAdd additional ground terms to SyGuS instantiation... tree | commitdiff
2020-10-01 Andrew ReynoldsUpdate theory of arithmetic to standard check (#5178) tree | commitdiff
2020-10-01 Aina NiemetzFloatingPoint: Add utility functions for largest and... tree | commitdiff
2020-10-01 Gereon KremerAllow to use the initial assignment for CAD (#5177) tree | commitdiff
2020-10-01 Andrew Reynolds(proof-new) Preprocessing passes use proper interfaces... tree | commitdiff
2020-10-01 Andrew ReynoldsMake SygusSolver use sygus attributes directly (#5172) tree | commitdiff
2020-10-01 Aina NiemetzBitVector: Extend interface of setBit to set it to... tree | commitdiff
2020-09-30 Aina NiemetzFloatingPoint: Add utility functions for largest and... tree | commitdiff
2020-09-30 Gereon KremerRemove too strict assertion to allow for approximate... tree | commitdiff
2020-09-30 Gereon KremerAdd missing includes. (#5170) tree | commitdiff
2020-09-30 Gereon KremerAdd strategy for nonlinear extension (#5160) tree | commitdiff
2020-09-30 Andrew ReynoldsDynamic allocation of equality engine for shared solver... tree | commitdiff
2020-09-30 Andrew Reynolds(proof-new) Add the term conversion sequence generator... tree | commitdiff
2020-09-29 Haniel Barbosa[proof-new] Adds a proof manager for prop engine (... tree | commitdiff
2020-09-29 mudathirmahgoubFix bags headers (#5165) tree | commitdiff
2020-09-29 Alex Ozdemir(proof-new) Add proof managers and eager gens to arith... tree | commitdiff
2020-09-29 Andrew Reynolds(proof-new) Fixes for preprocess proof generator and... tree | commitdiff
2020-09-29 Haniel Barbosa[proof-new] Adds a proof post processor for the Prop... tree | commitdiff
2020-09-29 Haniel Barbosa[proof-new] Updates to proof node updater (#5156) tree | commitdiff
2020-09-29 Haniel Barbosa[proof-new] Adds a proof-producing CNF converter (... tree | commitdiff
2020-09-29 Gereon KremerClean up nonlinear extension (#5149) tree | commitdiff
2020-09-29 Andrew ReynoldsReset assertions on resetAssertions (#5153) tree | commitdiff
2020-09-29 Alex OzdemirAdd utilities for arith/proof_checker and build it... tree | commitdiff
2020-09-29 Haniel Barbosa[proof-new] Removing spurious forward declaration in... tree | commitdiff
2020-09-29 Haniel Barbosa[proof-new] Adds a proof node hash function (#5154) tree | commitdiff
2020-09-28 Andrew ReynoldsMinor fixes to quantifiers proofs (#5151) tree | commitdiff
2020-09-28 Haniel Barbosa[proof-new] Adds a proof manager for the SAT solver... tree | commitdiff
2020-09-28 mudathirmahgoubImplement bags rewriter (#5132) tree | commitdiff
2020-09-28 Gereon KremerAdd new arithmetic BoundInference class (#5148) tree | commitdiff
2020-09-27 Andrew ReynoldsFix sygus quantifier elimination preprocess for multipl... tree | commitdiff
2020-09-26 Gereon KremerUse inference manager for nl_solver (#5125) tree | commitdiff
2020-09-26 Andrew ReynoldsConnect the shared solver to theory engine (#5103) tree | commitdiff
2020-09-26 Andrew ReynoldsUse original quantified formula for single invocation... tree | commitdiff
2020-09-26 Aina NiemetzRestrict bvxnor to only allow two operands (was n-ary... tree | commitdiff
2020-09-25 Andrew ReynoldsMake sygus refinement step more robust to unevaluatable... tree | commitdiff
2020-09-25 Haniel BarbosaCleaning and documenting cnf stream (#5134) tree | commitdiff
2020-09-24 Aina NiemetzSyGuS: Add default grammar for FP. (#5133) tree | commitdiff
2020-09-24 Andrew Reynolds Function definition fmf preprocessing pass (#5064) tree | commitdiff
2020-09-24 Andrew ReynoldsModify lemma vs fact policy for datatype equalities... tree | commitdiff
2020-09-23 Andrew ReynoldsDisable cegqi-bv when using sygus (#5124) tree | commitdiff
2020-09-23 Gereon KremerMake IAND solver use inference manager. (#5126) tree | commitdiff
2020-09-23 yoni206bv2int: new options for bvand translation (#5096) tree | commitdiff
2020-09-23 Andrew ReynoldsAllow E-matching by default when strings are enabled... tree | commitdiff
2020-09-23 Aina NiemetzNew C++ API: Catch and throw recoverable exception... tree | commitdiff
2020-09-23 Aina NiemetzFP: Use Assert instead of AlwaysAssert in traits::... tree | commitdiff
2020-09-23 Abdalrhman MohamedRefactor Commands to use the Public API. (#5105) tree | commitdiff
2020-09-23 Andrew ReynoldsFix type issue with term formula removal (#5107) tree | commitdiff
2020-09-23 Andres Noetzli[Python API] Conversion to/from Unicode strings (#5120) tree | commitdiff
2020-09-22 Aina NiemetzFP: Use Assert instead of PRECONDITION macro in convert... tree | commitdiff
2020-09-22 Mathias PreinerAdd simple BV solver (#5065) tree | commitdiff
2020-09-22 mudathirmahgoubAdd skeleton for theory of bags (multisets) (#5100) tree | commitdiff
2020-09-22 Andres NoetzliFix compilation without LibPoly (#5118) tree | commitdiff
2020-09-22 makaimannAdd method to get Python object from constant value... tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-22 Gereon KremerICP-based solver for nonlinear arithmetic (#5017) tree | commitdiff
2020-09-21 Andrew Reynolds(proof-new) Add the arrays proof checker (#5047) tree | commitdiff
2020-09-20 Andrew ReynoldsMore flexible design for model manager distributed... tree | commitdiff
2020-09-19 Andrew ReynoldsStandardize equality engine notifications in sets ... tree | commitdiff
2020-09-18 Andrew ReynoldsFix assertion list for globally defined recursive funct... tree | commitdiff
2020-09-18 Andrew ReynoldsAdd the shared solver (#4982) tree | commitdiff
2020-09-18 yoni206bv2int: quantifiers support (#5080) tree | commitdiff
2020-09-18 Andres NoetzliFix muzzled builds (#5093) tree | commitdiff
2020-09-18 Haniel Barbosa[proof-new] Proof utilities for normalizing clauses... tree | commitdiff
2020-09-18 Andrew ReynoldsLogic exception for arrays indexed by arrays (#5073) tree | commitdiff
2020-09-18 Andres Noetzli[Strings] Fix extended equality rewriter (#5092) tree | commitdiff
2020-09-18 Andrew Reynolds(proof-new) Updates to proof node updater algorithm... tree | commitdiff
2020-09-18 Andrew Reynolds(proof-new) Rewrites involving operators in term conver... tree | commitdiff
2020-09-17 Andrew Reynolds(proof-new) Fixes for theory engine proof generator... tree | commitdiff
2020-09-17 Haniel Barbosa[proof-new] Have mkScope agnostic to True assumptions... tree | commitdiff
2020-09-17 Gereon Kremer(cad-solver) Fix square-free-basis computation (#5085) tree | commitdiff
2020-09-17 Andrew ReynoldsReduce recursion in term formula removal (#5052) tree | commitdiff
2020-09-17 Gereon KremerUse new inference manager in transcendental solver... tree | commitdiff
2020-09-17 Andrew ReynoldsFurther standardization of datatypes (#5076) tree | commitdiff
2020-09-17 yoni206Dumping internal define-funs with no arguments (#5077) tree | commitdiff
2020-09-16 Andres NoetzliOnly rewrite replace_re(_all) if regexp is const (... tree | commitdiff
next