projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Add a new arith constraint proof rule: IntTightenAP (#3818)
[cvc5.git] / test /
2020-03-05 Andrew ReynoldsMigrate a majority of the functionality in parsers... tree | commitdiff
2020-03-05 Andrew ReynoldsFix issues with real to int (#3918) tree | commitdiff
2020-03-03 mudathirmahgoubRefactoring and cleaning the type enumerator for sets... tree | commitdiff
2020-02-29 Andrew Reynolds Throw warning instead of error for non-constant values... tree | commitdiff
2020-02-29 Andres NoetzliAdd support for str.from_code (#3829) tree | commitdiff
2020-02-29 Andrew ReynoldsFix assertion related to assignability in the model... tree | commitdiff
2020-02-29 Andrew ReynoldsReplace conditional rewrite pass in quantifiers with... tree | commitdiff
2020-02-27 Andrew ReynoldsFix large models for strings (#3835) tree | commitdiff
2020-02-27 Andrew ReynoldsAdd support for is_digit and regular expression differe... tree | commitdiff
2020-02-27 Andrew ReynoldsDisable regression that times out on debug (#3833) tree | commitdiff
2020-02-26 Andrew ReynoldsUse side effect utility for non-linear lemmas (#3780) tree | commitdiff
2020-02-26 Andrew ReynoldsFix regression (#3827) tree | commitdiff
2020-02-26 Andrew ReynoldsMore fixes for printing sygus commands (#3812) tree | commitdiff
2020-02-26 Andrew ReynoldsBasic support for regular expression complement (#3437) tree | commitdiff
2020-02-26 Andrew ReynoldsUse default consts when not using any const during... tree | commitdiff
2020-02-26 Andrew ReynoldsFix node arity issue in reduction of int2bv (#3777) tree | commitdiff
2020-02-26 Andrew ReynoldsSupport for witnessing choice in models (#3781) tree | commitdiff
2020-02-26 Andres NoetzliRemove portfolio leftovers (#3821) tree | commitdiff
2020-02-25 yoni206bv_to_int preprocessing pass tree | commitdiff
2020-02-24 Andrew ReynoldsUtilities for words (#3797) tree | commitdiff
2020-02-24 Andrew ReynoldsConvert parser input interface to api::Term (#3809) tree | commitdiff
2020-02-24 Andrew ReynoldsAdd missing functions to new C++ API (#3769) tree | commitdiff
2020-02-24 Andres NoetzliMake lambda rewriter more robust (#3806) tree | commitdiff
2020-02-22 Alex OzdemirSwitch to th_lira.plf (#3741) tree | commitdiff
2020-02-21 Aina NiemetzNew C++ API: Remove TOTAL kinds. (#3794) tree | commitdiff
2020-02-21 Andrew ReynoldsSimple changes towards unicode string standard (#3791) tree | commitdiff
2020-02-20 Andrew ReynoldsRemove front-end support for Chain (#3767) tree | commitdiff
2020-02-20 Mathias Preinerresource manager: Add statistic for every resource... tree | commitdiff
2020-02-19 makaimannAdd Python bindings using Cython -- see below for more... tree | commitdiff
2020-02-19 Andrew ReynoldsDelay enumerative instantiation if theory engine does... tree | commitdiff
2020-02-19 Andrew ReynoldsChange Record to shared_ptr (#3778) tree | commitdiff
2020-02-19 makaimannChange datatype selector/constructor/tester to terms... tree | commitdiff
2020-02-17 Andrew ReynoldsOption to limit the number of rounds of enumerative... tree | commitdiff
2020-02-17 Andrew Reynolds Fix soundness bug in reduction of integer div/mod... tree | commitdiff
2020-02-16 Andrew ReynoldsDisable regression (#3761) tree | commitdiff
2020-02-14 Andrew ReynoldsRemove quantifiers rewrite rules infrastructure (#3754) tree | commitdiff
2020-02-12 Andrew ReynoldsEnsure ext rewrites for associative ops dont throw... tree | commitdiff
2020-02-12 Mathias Preinerrun_regression: Distinguish between timeout and failure... tree | commitdiff
2020-02-11 Andrew ReynoldsFix term simplification based on entailment in quantifi... tree | commitdiff
2020-02-08 Andrew ReynoldsFix rewrite rules sat regressions (#3734) tree | commitdiff
2020-02-08 Andres NoetzliMake "unknown" non-critical for unsat cores check ... tree | commitdiff
2020-02-07 mudathirmahgoubUniveset Cardinality constraints for infinite types... tree | commitdiff
2020-02-07 Andrew ReynoldsRefactor check-model handling in SmtEngine (#3723) tree | commitdiff
2020-02-07 Andrew ReynoldsFix exact sqrt (#3721) tree | commitdiff
2020-02-04 Alex OzdemirRegression tests for arithmetic proofs. (#3701) tree | commitdiff
2020-02-04 Aina NiemetzIncrease regression test time limit to 1200s. (#3704) tree | commitdiff
2020-02-03 Andrew ReynoldsMinor fixes to regressions (#3702) tree | commitdiff
2020-02-03 mudathirmahgoubFix cardinality of uninterpreted types when univset... tree | commitdiff
2020-02-03 Andrew ReynoldsSplit on model values when repaired model from non... tree | commitdiff
2020-02-03 Andrew ReynoldsFix invariant template inference for trivially infeasib... tree | commitdiff
2020-02-03 Andrew ReynoldsFix corner case of empty domains in bounded fmf (#3690) tree | commitdiff
2020-02-03 Andrew ReynoldsExample inference utility (#3670) tree | commitdiff
2020-01-31 Andrew ReynoldsRefactor relevance vectors for asserted quantifiers... tree | commitdiff
2020-01-31 Andres NoetzliFix arithmetic rewriter for exponential (#3688) tree | commitdiff
2020-01-30 Andrew ReynoldsFix rep set increment for empty domains (#3682) tree | commitdiff
2020-01-30 Andrew ReynoldsMake eq chain an aggressive rewrite in extended rewrite... tree | commitdiff
2020-01-30 Andrew ReynoldsEliminate spurious postprocessing step for single invoc... tree | commitdiff
2020-01-30 Andrew ReynoldsEnsure literals in FMF decision strategies are in the... tree | commitdiff
2020-01-30 Andrew ReynoldsWeaken assertion for models with approximations (#3667) tree | commitdiff
2020-01-30 Andrew ReynoldsDo not debug check model for models with approximations... tree | commitdiff
2020-01-29 Andrew ReynoldsFix isLeq function in String utility (#3659) tree | commitdiff
2020-01-28 Andrew ReynoldsDo not insist on bound values being constant in arithme... tree | commitdiff
2020-01-28 Andrew ReynoldsAvoid PLUS with one child for bv2nat elimination (... tree | commitdiff
2020-01-23 Andrew ReynoldsFix trivial solve method for single invocation (#3650) tree | commitdiff
2020-01-22 Andrew ReynoldsFix subtyping for instantiations where internal represe... tree | commitdiff
2020-01-22 Andrew ReynoldsFix single invocation partition for non-function non... tree | commitdiff
2020-01-22 Andrew ReynoldsFix check for subtypes in sygus PBE (#3640) tree | commitdiff
2020-01-22 Andrew ReynoldsFix parameteric sorts involving Booleans in sygus defau... tree | commitdiff
2020-01-15 Aina NiemetzNew C++ API: Add nullary constructor for Result. (... tree | commitdiff
2020-01-14 Andrew ReynoldsGeneralize example-based sym breaking to conjectures... tree | commitdiff
2020-01-14 Andres NoetzliDisable unsat cores for regression that times out ... tree | commitdiff
2020-01-10 Andrew ReynoldsFix side condition check in sygus core connective ... tree | commitdiff
2020-01-10 Andres NoetzliFix printing of models of uninterpreted sorts (#3597) tree | commitdiff
2020-01-10 Andrew ReynoldsTrack trivial cases in transition inference (#3598) tree | commitdiff
2020-01-08 Andrew ReynoldsFix backtracking issue in sygus fast enumerator (#3593) tree | commitdiff
2020-01-08 mudathirmahgoubUniverse set cardinality for finite types with finite... tree | commitdiff
2020-01-07 Andrew ReynoldsUpdate any-constant and normalization policies for... tree | commitdiff
2020-01-04 Andrew ReynoldsFix finiteness check for bounded fmf (#3589) tree | commitdiff
2019-12-31 Alex Ozdemir[proof] ITE translation fix (#3484) tree | commitdiff
2019-12-23 Andrew ReynoldsInitial support for string reverse (#3581) tree | commitdiff
2019-12-18 Andrew ReynoldsIncrement Taylor degree for tangent and secant plane... tree | commitdiff
2019-12-18 Andres NoetzliAvoid calling rewriter from type checker (#3548) tree | commitdiff
2019-12-17 Andrew ReynoldsFix spurious parse error for rational real array consta... tree | commitdiff
2019-12-16 Ying ShengSupport ackermannization on uninterpreted sorts in... tree | commitdiff
2019-12-13 Andrew ReynoldsAdd support for set comprehension (#3312) tree | commitdiff
2019-12-13 Andrew ReynoldsDisable check-synth-sol in regression with recursive... tree | commitdiff
2019-12-12 Andrew ReynoldsMake CEGIS sampling robust to non-vanilla CEGIS (#3559) tree | commitdiff
2019-12-12 Haniel BarbosaFix Unif+PI algorithm with symbolic unfolding (#3558) tree | commitdiff
2019-12-12 Andrew ReynoldsFixes for regressions (#3557) tree | commitdiff
2019-12-12 Andrew ReynoldsFix CEGIS refinement for recursive functions evaluation... tree | commitdiff
2019-12-11 Andrew ReynoldsDo not substitute beneath arithmetic terms in the non... tree | commitdiff
2019-12-10 Haniel BarbosaFix ufho issues (#3551) tree | commitdiff
2019-12-10 Andrew ReynoldsAllow unsat cores with sygus inference (#3550) tree | commitdiff
2019-12-09 Andrew ReynoldsFix case of uninterpreted constant instantiation in... tree | commitdiff
2019-12-08 Andres Noetzli[Regressions] Require proof support for abduction ... tree | commitdiff
2019-12-07 Andres NoetzliSimplify rewrite for character matching (#3545) tree | commitdiff
2019-12-06 Andrew ReynoldsNew algorithm for interpolation and abduction based... tree | commitdiff
2019-12-06 Andrew ReynoldsAdd ExprManager as argument to Datatype (#3535) tree | commitdiff
2019-12-06 Alex Ozdemir[proof] Eliminate side-condition from ER signature... tree | commitdiff
2019-12-05 Andrew ReynoldsMake nonlinear solver intercept model assignments from... tree | commitdiff
next