projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2020-01-30 Andrew ReynoldsMake eq chain an aggressive rewrite in extended rewrite... commit | commitdiff | tree
2020-01-30 Andrew ReynoldsEliminate spurious postprocessing step for single invoc... commit | commitdiff | tree
2020-01-30 Andrew ReynoldsEnsure literals in FMF decision strategies are in the... commit | commitdiff | tree
2020-01-30 Andrew ReynoldsWeaken assertion for models with approximations (#3667) commit | commitdiff | tree
2020-01-30 Andrew ReynoldsMove disequality list to solver state in strings (... commit | commitdiff | tree
2020-01-30 Andrew ReynoldsExample minimize evaluation utility. (#3671) commit | commitdiff | tree
2020-01-30 Andrew ReynoldsExternal cache argument for evaluator (#3672) commit | commitdiff | tree
2020-01-30 Andrew ReynoldsDo not debug check model for models with approximations... commit | commitdiff | tree
2020-01-30 Andres NoetzliBetter heuristics for marking congruent variables ... commit | commitdiff | tree
2020-01-30 Andrew ReynoldsModularize more steps in the strings strategy (#3676) commit | commitdiff | tree
2020-01-30 Andrew ReynoldsMinor updates to string utilities (#3675) commit | commitdiff | tree
2020-01-30 Alex OzdemirexpectedType in proof-printing code (#3665) commit | commitdiff | tree
2020-01-29 Andrew ReynoldsFix isLeq function in String utility (#3659) commit | commitdiff | tree
2020-01-28 Andrew ReynoldsDo not insist on bound values being constant in arithme... commit | commitdiff | tree
2020-01-28 Andrew ReynoldsAvoid PLUS with one child for bv2nat elimination (... commit | commitdiff | tree
2020-01-26 Alex OzdemirAxioms for affine function bounds. Tests. (#3632) commit | commitdiff | tree
2020-01-23 Andrew ReynoldsFix trivial solve method for single invocation (#3650) commit | commitdiff | tree
2020-01-22 Andrew ReynoldsFix subtyping for instantiations where internal represe... commit | commitdiff | tree
2020-01-22 Andrew ReynoldsFix substitution in nl solver (#3638) commit | commitdiff | tree
2020-01-22 Andrew ReynoldsFix single invocation partition for non-function non... commit | commitdiff | tree
2020-01-22 Andrew ReynoldsFix check for subtypes in sygus PBE (#3640) commit | commitdiff | tree
2020-01-22 Andrew ReynoldsFix parameteric sorts involving Booleans in sygus defau... commit | commitdiff | tree
2020-01-21 Alex OzdemirTypes and side conditions for affine bounds (#3631) commit | commitdiff | tree
2020-01-21 Alex OzdemirAffine Axioms (#3630) commit | commitdiff | tree
2020-01-21 Alex OzdemirTypes & side-conditions for linear and affine fns ... commit | commitdiff | tree
2020-01-21 Alex OzdemirAxioms (and side conditions) for tightening bounds... commit | commitdiff | tree
2020-01-18 Alex OzdemirLIRA proof: Arithmetic predicates & reification thereof... commit | commitdiff | tree
2020-01-17 Alex OzdemirLIRA sig: int, real terms, and conversions (#3610) commit | commitdiff | tree
2020-01-17 Andrew ReynoldsUse axioms when checking goal entailment for abduction... commit | commitdiff | tree
2020-01-15 Aina NiemetzNew C++ API: Add nullary constructor for Result. (... commit | commitdiff | tree
2020-01-14 Andrew ReynoldsGeneralize example-based sym breaking to conjectures... commit | commitdiff | tree
2020-01-14 Andres NoetzliDisable unsat cores for regression that times out ... commit | commitdiff | tree
2020-01-13 Andres NoetzliSupport arbitrary unsigned integer attributes (#3591) commit | commitdiff | tree
2020-01-10 Andrew ReynoldsFix side condition check in sygus core connective ... commit | commitdiff | tree
2020-01-10 Mathias PreinerFix enum names in AIG bitblaster. (#3599) commit | commitdiff | tree
2020-01-10 Andres NoetzliFix printing of models of uninterpreted sorts (#3597) commit | commitdiff | tree
2020-01-10 Andrew ReynoldsTrack trivial cases in transition inference (#3598) commit | commitdiff | tree
2020-01-10 Andres NoetzliOptimize str.substr reduction (#3595) commit | commitdiff | tree
2020-01-08 Andrew ReynoldsFix backtracking issue in sygus fast enumerator (#3593) commit | commitdiff | tree
2020-01-08 mudathirmahgoubUniverse set cardinality for finite types with finite... commit | commitdiff | tree
2020-01-07 Andrew ReynoldsFix unary minus parse check (#3594) commit | commitdiff | tree
2020-01-07 Andrew ReynoldsUpdate any-constant and normalization policies for... commit | commitdiff | tree
2020-01-04 Andrew ReynoldsFix finiteness check for bounded fmf (#3589) commit | commitdiff | tree
2019-12-31 Alex Ozdemir[proof] ITE translation fix (#3484) commit | commitdiff | tree
2019-12-23 Andrew ReynoldsInitial support for string reverse (#3581) commit | commitdiff | tree
2019-12-19 Simon DierlDefine all options modified by ENABLE_BEST using cvc4_o... commit | commitdiff | tree
2019-12-19 Mathias PreinerFix typo in smt_options.toml. (#3579) commit | commitdiff | tree
2019-12-18 Andrew ReynoldsIncrement Taylor degree for tangent and secant plane... commit | commitdiff | tree
2019-12-18 Andres NoetzliAvoid calling rewriter from type checker (#3548) commit | commitdiff | tree
2019-12-17 Mathias PreinerGenerate code for options with modes. (#3561) commit | commitdiff | tree
2019-12-17 Andrew ReynoldsFix spurious parse error for rational real array consta... commit | commitdiff | tree
2019-12-16 Andrew ReynoldsUse the evaluator utility in the function definition... commit | commitdiff | tree
2019-12-16 Andrew ReynoldsExtend model construction with assignment exclusion... commit | commitdiff | tree
2019-12-16 Ying ShengSupport ackermannization on uninterpreted sorts in... commit | commitdiff | tree
2019-12-16 Andrew ReynoldsMove Datatype management to ExprManager (#3568) commit | commitdiff | tree
2019-12-16 Andrew ReynoldsFix evaluator for non-evaluatable nodes (#3575) commit | commitdiff | tree
2019-12-16 Andrew ReynoldsRevert evaluate as node. (#3574) commit | commitdiff | tree
2019-12-16 makaimannTrace tags for dumping the decision tree in org-mode... commit | commitdiff | tree
2019-12-16 Andrew ReynoldsMinor improvement to evaluator (#3570) commit | commitdiff | tree
2019-12-15 Andrew ReynoldsSimple optimizations for the core rewriter (#3569) commit | commitdiff | tree
2019-12-13 Andrew ReynoldsEliminate Expr-level calls in TypeNode (#3562) commit | commitdiff | tree
2019-12-13 Andrew ReynoldsAdd support for set comprehension (#3312) commit | commitdiff | tree
2019-12-13 Andrew ReynoldsDisable check-synth-sol in regression with recursive... commit | commitdiff | tree
2019-12-13 Aina Niemetz FP converter: convert: Use std::vector as instead... commit | commitdiff | tree
2019-12-12 Andrew ReynoldsMake CEGIS sampling robust to non-vanilla CEGIS (#3559) commit | commitdiff | tree
2019-12-12 Haniel BarbosaFix Unif+PI algorithm with symbolic unfolding (#3558) commit | commitdiff | tree
2019-12-12 Andrew ReynoldsUse the node-level datatypes API (#3556) commit | commitdiff | tree
2019-12-12 Andrew ReynoldsFixes for regressions (#3557) commit | commitdiff | tree
2019-12-12 Andrew ReynoldsFix CEGIS refinement for recursive functions evaluation... commit | commitdiff | tree
2019-12-12 Andrew ReynoldsActivate node-level datatype API (#3540) commit | commitdiff | tree
2019-12-11 Andrew ReynoldsDo not substitute beneath arithmetic terms in the non... commit | commitdiff | tree
2019-12-11 Andrew ReynoldsSupport symbolic unfolding in UNIF+PI (#3553) commit | commitdiff | tree
2019-12-10 Andrew ReynoldsIncorporate rewriting on demand in the evaluator (... commit | commitdiff | tree
2019-12-10 Haniel BarbosaFix ufho issues (#3551) commit | commitdiff | tree
2019-12-10 Andrew ReynoldsAllow unsat cores with sygus inference (#3550) commit | commitdiff | tree
2019-12-09 Andrew ReynoldsDisable sygus inference when combined with incremental... commit | commitdiff | tree
2019-12-09 Andrew ReynoldsFix case of uninterpreted constant instantiation in... commit | commitdiff | tree
2019-12-09 Andres NoetzliMake theory rewriters non-static (#3547) commit | commitdiff | tree
2019-12-08 Andres Noetzli[Regressions] Require proof support for abduction ... commit | commitdiff | tree
2019-12-07 Andres NoetzliSimplify rewrite for character matching (#3545) commit | commitdiff | tree
2019-12-07 Andres NoetzliUse str.subtr in str.to.int/int.to.str reduction (... commit | commitdiff | tree
2019-12-06 Andrew ReynoldsThrow exception instead of warning for approximate... commit | commitdiff | tree
2019-12-06 Andres NoetzliAdd lemma for str.to.int/int.to.str (#3541) commit | commitdiff | tree
2019-12-06 Andrew ReynoldsOptimize the rewriter for DT_SYGUS_EVAL (#3529) commit | commitdiff | tree
2019-12-06 Andrew ReynoldsNew algorithm for interpolation and abduction based... commit | commitdiff | tree
2019-12-06 Andrew ReynoldsAdd ExprManager as argument to Datatype (#3535) commit | commitdiff | tree
2019-12-06 Alex Ozdemir[proof] Eliminate side-condition from ER signature... commit | commitdiff | tree
2019-12-06 Mathias Preinercontrib: Setup all dependencies in deps/ directory... commit | commitdiff | tree
2019-12-06 Andrew ReynoldsIntroduce the Node-level Datatypes API (#3462) commit | commitdiff | tree
2019-12-05 Andrew ReynoldsMake nonlinear solver intercept model assignments from... commit | commitdiff | tree
2019-12-05 Andrew ReynoldsRefactor mode options for Unif+PI (#3531) commit | commitdiff | tree
2019-12-05 Andres NoetzliBi-directional unrolling of R* regular expressions... commit | commitdiff | tree
2019-12-05 makaimannAdd mkOp for a single Kind (#3522) commit | commitdiff | tree
2019-12-05 Andrew ReynoldsFix the subtyping relation for functions (#3494) commit | commitdiff | tree
2019-12-04 Andrew ReynoldsNew grammar construction modes for SyGuS (#3486) commit | commitdiff | tree
2019-12-04 Andrew ReynoldsFix (#3530) commit | commitdiff | tree
2019-12-04 Andrew ReynoldsFixes for SyGuS PBE + templated string concatenations... commit | commitdiff | tree
2019-12-04 Andrew ReynoldsFix single invocation solution construction for multipl... commit | commitdiff | tree
2019-12-04 Andres NoetzliFix corner case in model construction of strings (... commit | commitdiff | tree
2019-12-03 Andrew ReynoldsImprove flexibility of lemma output in non-linear solve... commit | commitdiff | tree
next