projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Statistics on instantiations per quantified formula. (#4719)
[cvc5.git] / src / theory / arith /
2020-07-11 Andrew Reynolds(proof-new) Update Theory interface for proof-new ... tree | commitdiff
2020-07-09 Andrew ReynoldsAssociate all lemmas in non-linear arithmetic with... tree | commitdiff
2020-07-08 Andrew ReynoldsImprove and fix secant and tangent lemmas in the transc... tree | commitdiff
2020-07-01 Andrew ReynoldsAdd solver for integer AND (#4681) tree | commitdiff
2020-06-30 Andrew ReynoldsAdd internal support for integer and operator (#4668) tree | commitdiff
2020-06-28 Alex OzdemirProof Rules and Checker for Arithmetic (#4665) tree | commitdiff
2020-06-25 Andrew ReynoldsUpdate option --nl-ext to enable/disable incremental... tree | commitdiff
2020-06-22 Andrew ReynoldsAdd trascendental function kinds to list of unevaluated... tree | commitdiff
2020-06-19 Andrew Reynolds(proof-new) Split operator elimination from arithmetic... tree | commitdiff
2020-06-16 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-06-11 Andrew Reynolds(proof-new) Remove arith-snorm option. (#4591) tree | commitdiff
2020-06-08 Andres NoetzliFix Coverity issues (#4587) tree | commitdiff
2020-06-06 Andrew ReynoldsUse NlLemma utility for all lemmas in non-linear. ... tree | commitdiff
2020-06-05 Andrew Reynolds(proof-new) Rename ProofSkolemCache to SkolemManager... tree | commitdiff
2020-06-01 Andrew ReynoldsMove non-linear files to src/theory/arith/nl (#4548) tree | commitdiff
2020-05-31 Andres NoetzliDo not cache operator eliminations in arith (#4542) tree | commitdiff
2020-05-23 Andrew ReynoldsRefactor operator elimination in arithmetic (#4519) tree | commitdiff
2020-05-20 Andrew ReynoldsDo not eliminate variables that are equal to unevaluata... tree | commitdiff
2020-05-19 mudathirmahgoubRenamed operator CHOICE to WITNESS (#4207) tree | commitdiff
2020-04-11 Andrew ReynoldsSplit the non-linear solver (#4219) tree | commitdiff
2020-04-08 Andres NoetzliPerform theory widening eagerly (#4044) tree | commitdiff
2020-04-03 Andres NoetzliUpdate theory rewriter ownership, add stats to strings... tree | commitdiff
2020-04-02 Andres NoetzliInitialize theory rewriters in theories (#4197) tree | commitdiff
2020-03-28 Andrew ReynoldsSplit transcendental solver to its own file (#4156) tree | commitdiff
2020-03-26 AmaleeAdded unit-cube-like test for branch and bound (#3922) tree | commitdiff
2020-03-23 Andrew ReynoldsChange transcendental function app slave list to unorde... tree | commitdiff
2020-03-16 Alex Ozdemirclang-format tree | commitdiff
2020-03-16 Alex OzdemirFix simplicity check in prop tree | commitdiff
2020-03-16 Alex OzdemirFix antecedent loop. Whoops tree | commitdiff
2020-03-16 Alex OzdemirOnly save farkas+tightening proofs. Error on holes tree | commitdiff
2020-03-16 Alex OzdemirExpand the definition of a "simple" farkas proof. tree | commitdiff
2020-03-10 Andrew ReynoldsRemove assertion in resolution bound inferences (#3980) tree | commitdiff
2020-03-10 Andrew ReynoldsDo not set values for non-linear mult terms in collectM... tree | commitdiff
2020-03-09 Andrew ReynoldsFix type issue in arith rewrite equality (#3972) tree | commitdiff
2020-03-09 Andrew ReynoldsFixes for bounds on transcendental functions (#3832) tree | commitdiff
2020-03-09 Andrew ReynoldsRewrite again full for DIV rewrite (#3945) tree | commitdiff
2020-03-05 Alex OzdemirAdd a new arith constraint proof rule: IntTightenAP... tree | commitdiff
2020-03-05 Alex OzdemirRevert "Add a new arith constraint proof rule: IntTight... tree | commitdiff
2020-03-05 Andres NoetzliAdd a new arith constraint proof rule: IntTightenAP... tree | commitdiff
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) tree | commitdiff
2020-02-27 Andrew ReynoldsInitial work towards -Wshadow (#3817) tree | commitdiff
2020-02-26 Andrew ReynoldsInfrastructure for tautological literals in nonlinear... tree | commitdiff
2020-02-26 Andrew ReynoldsUse side effect utility for non-linear lemmas (#3780) tree | commitdiff
2020-02-26 Andrew ReynoldsSupport for witnessing choice in models (#3781) tree | commitdiff
2020-02-20 Mathias Preinerresource manager: Add statistic for every resource... tree | commitdiff
2020-02-19 Andrew ReynoldsFix approximate bounds for transcendental functions... tree | commitdiff
2020-02-17 Andrew Reynolds Fix soundness bug in reduction of integer div/mod... tree | commitdiff
2020-02-12 Andrew ReynoldsFix non-linear equality solving that involves mixed... tree | commitdiff
2020-02-07 Andrew ReynoldsFix exact sqrt (#3721) tree | commitdiff
2020-02-04 Alex OzdemirArticulate proof-related debug statements in arith... tree | commitdiff
2020-02-03 Andrew ReynoldsSplit on model values when repaired model from non... tree | commitdiff
2020-01-31 Andres NoetzliFix arithmetic rewriter for exponential (#3688) tree | commitdiff
2020-01-22 Andrew ReynoldsFix substitution in nl solver (#3638) tree | commitdiff
2019-12-18 Andrew ReynoldsIncrement Taylor degree for tangent and secant plane... tree | commitdiff
2019-12-17 Mathias PreinerGenerate code for options with modes. (#3561) tree | commitdiff
2019-12-11 Andrew ReynoldsDo not substitute beneath arithmetic terms in the non... tree | commitdiff
2019-12-09 Andres NoetzliMake theory rewriters non-static (#3547) tree | commitdiff
2019-12-05 Andrew ReynoldsMake nonlinear solver intercept model assignments from... tree | commitdiff
2019-12-03 Andrew ReynoldsImprove flexibility of lemma output in non-linear solve... tree | commitdiff
2019-12-02 makaimannOpTerm Refactor: Allow retrieving OpTerm used to create... tree | commitdiff
2019-11-22 Andrew ReynoldsMinor refactoring of compute model value for nl (#3489) tree | commitdiff
2019-11-19 Andres NoetzliFix reduction of `sqrt` (#3478) tree | commitdiff
2019-11-18 Andres NoetzliUse -Wimplicit-fallthrough (#3464) tree | commitdiff
2019-11-13 Andrew ReynoldsRefactor non-linear extension for model-based refinemen... tree | commitdiff
2019-11-05 Andrew ReynoldsSeparate model object in non-linear extension (#3426) tree | commitdiff
2019-10-31 Mathias PreinerFix Unimplemented() macros missed in #3366. (#3424) tree | commitdiff
2019-10-30 Mathias PreinerUnify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ... tree | commitdiff
2019-10-30 Andrew ReynoldsSplit some generic utilities from the non-linear extens... tree | commitdiff
2019-10-28 Andrew ReynoldsFix for non-linear models (#3410) tree | commitdiff
2019-10-28 Andres NoetzliFix integer division rewrite (#3415) tree | commitdiff
2019-10-13 Andrew ReynoldsEliminate negative constant coefficients in div/mod... tree | commitdiff
2019-10-08 Piotr Trojanekprefer prefix ++ operator for iterators tree | commitdiff
2019-09-29 Andres NoetzliIntroduce template classes for simple type rules (... tree | commitdiff
2019-09-04 Andrew Reynolds Fixes related to destructing null (#3231) tree | commitdiff
2019-08-24 Piotr Trojanekfix mismatch between "delete" and "new []" (#2795) tree | commitdiff
2019-08-23 Andrew ReynoldsFix argument in nonlinear extension. (#3216) tree | commitdiff
2019-06-11 Ahmed IrfanNA Tangent reverse implication (#3050) tree | commitdiff
2019-04-24 Mathias PreinerDo not use __ prefix for header guards. (#2974) tree | commitdiff
2019-03-26 Aina NiemetzUpdate copyright headers. tree | commitdiff
2019-03-14 Andrew ReynoldsUse zero slope tangent planes for transcendental functi... tree | commitdiff
2019-01-03 Alex Ozdemir[LRA proof] Recording & Printing LRA Proofs (#2758) tree | commitdiff
2018-12-20 Aina NiemetzAdd missing type rules for parameterized operator kinds... tree | commitdiff
2018-12-15 Alex Ozdemir [LRA Proof] Storage for LRA proofs (#2747) tree | commitdiff
2018-12-14 Aina NiemetzFixed typos. tree | commitdiff
2018-12-07 Alex OzdemirArith Constraint Proof Loggin (#2732) tree | commitdiff
2018-10-01 Aina NiemetzFix compiler warnings. (#2555) tree | commitdiff
2018-09-27 Andrew ReynoldsFix Taylor overapproximation for large exponentials... tree | commitdiff
2018-09-25 Andrew Reynolds Improve non-linear check model error handling (#2497) tree | commitdiff
2018-09-22 Mathias Preinercmake: Remove unused CMakeLists.txt tree | commitdiff
2018-09-22 Aina Niemetzcmake: Added initial build infrastructure. tree | commitdiff
2018-09-13 Andrew ReynoldsSimplify storing of transcendental function application... tree | commitdiff
2018-09-13 Andrew Reynolds Decision strategy: incorporate CEGQI (#2460) tree | commitdiff
2018-09-05 Mathias PreinerUse std::uniqe_ptr for d_eq_infer to make Coverity... tree | commitdiff
2018-08-30 Andres NoetzliUse useBland option in FCSimplexDecisionProcedure ... tree | commitdiff
2018-08-23 Aina NiemetzRefactor ITE simplification preprocessing pass. (#2360) tree | commitdiff
2018-08-16 Andres NoetzliMove node algorithms to separate file (#2311) tree | commitdiff
2018-08-08 Andres NoetzliRequire Swig 3 (#2283) tree | commitdiff
2018-07-26 Tim KingChanging the arithmetic static learner to use CDHashMap... tree | commitdiff
2018-07-25 Tim KingChanging ArithIteUtils to use CDInsertHashMap. (#2206) tree | commitdiff
2018-07-17 Andrew Reynolds Purify applications of exp to transcendental arguments... tree | commitdiff
next