cvc5.git
2021-01-08 yoni206bv-to-int: avoid binarizing nodes twice (#5749)
2021-01-07 Gereon KremerMake sure polynomials are properly factorized in nl...
2021-01-07 Haniel BarbosaRemove dependency on expression layer in TPTP parser...
2021-01-07 Haniel BarbosaFix warning in TPTP parser (#5752)
2021-01-06 yoni206strings arith checks preprocessing pass: step 1 (#5747)
2021-01-06 Andrew ReynoldsAdd new interfaces to term formula removal and theory...
2021-01-05 yoni206Adding str.len to triggers (#5746)
2021-01-05 Andrew ReynoldsRemove a few miscellaneous references to the expr layer...
2020-12-24 Haniel Barbosa[proof-new] Only use old proofs for unsat cores if...
2020-12-23 Haniel BarbosaDumping unsat cores after check-sat-assuming/QUERY...
2020-12-23 Andrew ReynoldsAdd option to track and notify from CNF stream (#5708)
2020-12-23 Andrew ReynoldsRemove quant EPR option (#5716)
2020-12-23 Haniel Barbosa[proof-new] Adding a manager for the new unsat cores...
2020-12-23 Andrew Reynolds(proof-new) Miscelleneous fixes from proof-new (#5714)
2020-12-23 Gereon KremerAdd proofs for nonlinear sign lemmas. (#5707)
2020-12-23 Andrew ReynoldsMinor simplification to Theory::theoryOf (#5719)
2020-12-22 yoni206Delete duplicated code (#5718)
2020-12-22 Andrew ReynoldsMove slow regression to regress3 (#5715)
2020-12-22 Andrew ReynoldsMake theory preprocess rewrite equalities a preprocessi...
2020-12-22 Andrew ReynoldsRemove preregister instantiation heuristic (#5713)
2020-12-21 Gereon KremerAdd proof for pi bound lemma (#5709)
2020-12-21 Haniel BarbosaHave unsat core regression agnostic to number of assert...
2020-12-21 Andrew ReynoldsMove ownership of theory preprocessor to TheoryProxy...
2020-12-21 Gereon KremerAdd proof for sine shift lemmas. (#5710)
2020-12-21 Gereon Kremer(proof-new) Make nl-ext factoring lemmas proof producin...
2020-12-21 Andrew ReynoldsEliminate recursion from the internals of term formula...
2020-12-21 Andrew ReynoldsFix issue with selector triggers (#5689)
2020-12-18 Gereon Kremer(proof-new) Setup proof infrastructure for transcendent...
2020-12-18 Andrew ReynoldsSimplify internal API for sygus (#5687)
2020-12-18 Gereon KremerAdd proof checker for nl tangent lemma (#5704)
2020-12-18 Alex OzdemirBugfix: proofs for props of non-normal arith lits ...
2020-12-18 Gereon Kremer(proof-new) Add proof for tangent plane lemmas (#5700)
2020-12-18 Gereon KremerAdd proof for split zero check. (#5699)
2020-12-17 Andrew Reynolds(proof-new) Minor updates to term conversion proof...
2020-12-17 Gereon KremerAlways consider rewritten lemmas for caching. (#5696)
2020-12-17 Gereon Kremer(proof-new) Prepare nonlinear extension and nl-ext...
2020-12-17 Andrew ReynoldsSimplify term formula removal interface (#5695)
2020-12-17 Andrew ReynoldsSimplify and fix check models (#5685)
2020-12-17 Haniel Barbosa[proof-new] Only use old proof code for unsat cores...
2020-12-16 Andrew ReynoldsSimplify preprocessing (#5647)
2020-12-16 Andrew ReynoldsMark quantifier instantiations as needs justify (#5684)
2020-12-16 Andrew ReynoldsSimplify synth-fun printer (#5682)
2020-12-16 mudathirmahgoubRenamed InferInfo::getAntecedant to InferInfo::getAntec...
2020-12-16 Andrew Reynolds(proof-new) Use bound variable manager (#5679)
2020-12-16 Andrew ReynoldsMove ownership of term formula removal to theory prepro...
2020-12-16 Andrew ReynoldsUse uint64 utility when parsing tuple selectors in...
2020-12-15 Andrew ReynoldsMove trigger trie to own file (#5680)
2020-12-15 Andrew ReynoldsImprovements related to quantifiers printing (#5678)
2020-12-15 Andrew ReynoldsProper expand definitions for sets (#5676)
2020-12-15 Andrew ReynoldsConsolidate basic sygus utilities regarding sygus conje...
2020-12-15 Andrew ReynoldsFix datatypes compute ground value (#5671)
2020-12-15 Andrew ReynoldsRemove bv divide by zero option (#5672)
2020-12-15 Gereon KremerAdd getters to retrieve constants from api::Term (...
2020-12-14 Haniel Barbosa[proof-new] Making the CDCL(T) Minisat proof producing...
2020-12-14 Haniel Barbosa[proof-new] Make prop engine proof producing (#5667)
2020-12-14 Andrew ReynoldsProperly implement datatype selector triggers (#5624)
2020-12-14 Haniel Barbosa[proof-new] Updating interfaces between prop engine...
2020-12-14 Andrew Reynolds(proof-new) Add bound variable manager (#5655)
2020-12-14 Andrew ReynoldsFix and improve evaluator (#5563)
2020-12-14 Andrew ReynoldsFix SAT-context dependent issue in strings preregistrat...
2020-12-12 Andrew ReynoldsFlush statistics through NodeManager in SmtEngine ...
2020-12-11 yoni206bv-to-int: new tests from an issue (#5654)
2020-12-11 Haniel Barbosa [proof-new] Updating theory proxy to new proof infrast...
2020-12-11 Andrew ReynoldsFix length assumption for deq norm emp rule (#5623)
2020-12-10 Gereon KremerRefactor KindMap (#5646)
2020-12-10 Aina Niemetzgoogle test: expr: Migrate node_algorithm_black. (...
2020-12-10 Andrew ReynoldsRefactor regressions (#5639)
2020-12-10 Aina Niemetzgoogle test: expr: Migrate kind_black. (#5634)
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637)
2020-12-09 Aina NiemetzFix compiler warnings. (#5644)
2020-12-09 Andrew Reynolds(proof-new) Make theory preprocessor proofs self contai...
2020-12-09 Aina Niemetzgoogle test: expr: Migrate kind_map_black. (#5640)
2020-12-09 Aina Niemetzkind_map: Remove unused Accessor class. (#5641)
2020-12-09 Aina Niemetzgoogle test: expr: Migrate attribute_white. (#5632)
2020-12-09 Andrew ReynoldsMake decision engine independent of AssertionsPipeline...
2020-12-09 Andrew ReynoldsRemove obsolete regressions (#5633)
2020-12-09 Aina Niemetzgoogle test: context: Migrate context_white. (#5630)
2020-12-09 Gereon KremerSplit initial exp lemma into separate lemmas. (#5622)
2020-12-09 Aina NiemetzDelete obsolete unit tests for Expr and ExprManager...
2020-12-09 Andrew ReynoldsEnsure CEGQI is applied for parametric datatypes when...
2020-12-09 Andrew ReynoldsDo not check FP at last call if not necessary (#5627)
2020-12-09 Aina Niemetzite_utilities: Fix infinite loop in compressTerm. ...
2020-12-09 yoni206update doc (#5619)
2020-12-08 Aina Niemetzgoogle test: context: Migrate context_mm_black. (#5592)
2020-12-08 Aina Niemetzgoogle test: context: Migrate context_black. (#5587)
2020-12-08 Gereon KremerAdd regression from #1978. (#5552)
2020-12-08 Abdalrhman... Fix a bug with synth-fun printer (#5512)
2020-12-08 Haniel Barbosa[proof-new] Updating SAT proof to use MACRO_RESOLUTION...
2020-12-08 yoni206bv-to-int: Expand definitions of bvudiv and bvurem...
2020-12-08 Andrew ReynoldsMake term indices in the strings base solver aware...
2020-12-08 Andrew ReynoldsProper implementation of expand definitions for sequenc...
2020-12-08 Andrew ReynoldsFix collect model values for sequences of sequences...
2020-12-08 Haniel Barbosa[proof-new] Adding MACRO_RESOLUTION rule and updating...
2020-12-08 Mathias PreinerAdd support for BV proofs with the simple bitblasting...
2020-12-08 Mathias PreinerDisable algebraic BV subtheory by default and make...
2020-12-07 Andrew ReynoldsFix and reenable fact vs lemma optimization in datatype...
2020-12-07 makaimannAdd bitwise refinement mode for IAND (#5328)
2020-12-07 Andrew ReynoldsFix issue with free variables introduced by quantifier...
2020-12-07 Gereon KremerRefactor initial phase of transcendental solver (#5599)
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of...
next