git.libre-soc.org Git - cvc5.git/search

2020-02-03	Andrew Reynolds	Minor fixes to regressions (#3702)	commit \| commitdiff \| tree
2020-02-03	mudathirmahgoub	Fix cardinality of uninterpreted types when univset...	commit \| commitdiff \| tree
2020-02-03	Andrew Reynolds	Split on model values when repaired model from non...	commit \| commitdiff \| tree
2020-02-03	Andrew Reynolds	Fix invariant template inference for trivially infeasible...	commit \| commitdiff \| tree
2020-02-03	Andrew Reynolds	Fix corner case of empty domains in bounded fmf (#3690)	commit \| commitdiff \| tree
2020-02-03	Andrew Reynolds	Example inference utility (#3670)	commit \| commitdiff \| tree
2020-02-03	Andrew V. Jones	Renaming '--bsd' to '--no-gpl' (#3609)	commit \| commitdiff \| tree
2020-02-01	Alex Ozdemir	Handle `expectedType` in TheoryProofEngine (#3691)	commit \| commitdiff \| tree
2020-01-31	Andrew Reynolds	Allow PBE symmetry breaking with sygus stream (#3686)	commit \| commitdiff \| tree
2020-01-31	Andrew Reynolds	Refactor relevance vectors for asserted quantifiers...	commit \| commitdiff \| tree
2020-01-31	Andrew Reynolds	Update sygus grammar normalization to use node-level...	commit \| commitdiff \| tree
2020-01-31	Andrew Reynolds	Refactor sygus stats (#3684)	commit \| commitdiff \| tree
2020-01-31	Andrew Reynolds	Minor refactoring of constructor classes in fast enumerator...	commit \| commitdiff \| tree
2020-01-31	Andres Noetzli	Fix arithmetic rewriter for exponential (#3688)	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Fix rep set increment for empty domains (#3682)	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Make eq chain an aggressive rewrite in extended rewriter...	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Eliminate spurious postprocessing step for single invocation...	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Ensure literals in FMF decision strategies are in the...	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Weaken assertion for models with approximations (#3667)	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Move disequality list to solver state in strings (...	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Example minimize evaluation utility. (#3671)	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	External cache argument for evaluator (#3672)	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Do not debug check model for models with approximations...	commit \| commitdiff \| tree
2020-01-30	Andres Noetzli	Better heuristics for marking congruent variables ...	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Modularize more steps in the strings strategy (#3676)	commit \| commitdiff \| tree
2020-01-30	Andrew Reynolds	Minor updates to string utilities (#3675)	commit \| commitdiff \| tree
2020-01-30	Alex Ozdemir	expectedType in proof-printing code (#3665)	commit \| commitdiff \| tree
2020-01-29	Andrew Reynolds	Fix isLeq function in String utility (#3659)	commit \| commitdiff \| tree
2020-01-28	Andrew Reynolds	Do not insist on bound values being constant in arithmetic...	commit \| commitdiff \| tree
2020-01-28	Andrew Reynolds	Avoid PLUS with one child for bv2nat elimination (...	commit \| commitdiff \| tree
2020-01-26	Alex Ozdemir	Axioms for affine function bounds. Tests. (#3632)	commit \| commitdiff \| tree
2020-01-23	Andrew Reynolds	Fix trivial solve method for single invocation (#3650)	commit \| commitdiff \| tree
2020-01-22	Andrew Reynolds	Fix subtyping for instantiations where internal representati...	commit \| commitdiff \| tree
2020-01-22	Andrew Reynolds	Fix single invocation partition for non-function non...	commit \| commitdiff \| tree
2020-01-22	Andrew Reynolds	Fix check for subtypes in sygus PBE (#3640)	commit \| commitdiff \| tree
2020-01-22	Andrew Reynolds	Fix parameteric sorts involving Booleans in sygus default...	commit \| commitdiff \| tree
2020-01-21	Alex Ozdemir	Types and side conditions for affine bounds (#3631)	commit \| commitdiff \| tree
2020-01-21	Alex Ozdemir	Affine Axioms (#3630)	commit \| commitdiff \| tree
2020-01-21	Alex Ozdemir	Types & side-conditions for linear and affine fns ...	commit \| commitdiff \| tree
2020-01-21	Alex Ozdemir	Axioms (and side conditions) for tightening bounds...	commit \| commitdiff \| tree
2020-01-18	Alex Ozdemir	LIRA proof: Arithmetic predicates & reification thereof...	commit \| commitdiff \| tree
2020-01-17	Alex Ozdemir	LIRA sig: int, real terms, and conversions (#3610)	commit \| commitdiff \| tree
2020-01-17	Andrew Reynolds	Use axioms when checking goal entailment for abduction...	commit \| commitdiff \| tree
2020-01-15	Aina Niemetz	New C++ API: Add nullary constructor for Result. (...	commit \| commitdiff \| tree
2020-01-14	Andrew Reynolds	Generalize example-based sym breaking to conjectures...	commit \| commitdiff \| tree
2020-01-14	Andres Noetzli	Disable unsat cores for regression that times out ...	commit \| commitdiff \| tree
2020-01-13	Andres Noetzli	Support arbitrary unsigned integer attributes (#3591)	commit \| commitdiff \| tree
2020-01-10	Andrew Reynolds	Fix side condition check in sygus core connective ...	commit \| commitdiff \| tree
2020-01-10	Mathias Preiner	Fix enum names in AIG bitblaster. (#3599)	commit \| commitdiff \| tree
2020-01-10	Andrew Reynolds	Track trivial cases in transition inference (#3598)	commit \| commitdiff \| tree
2020-01-10	Andres Noetzli	Optimize str.substr reduction (#3595)	commit \| commitdiff \| tree
2020-01-08	Andrew Reynolds	Fix backtracking issue in sygus fast enumerator (#3593)	commit \| commitdiff \| tree
2020-01-08	mudathirmahgoub	Universe set cardinality for finite types with finite...	commit \| commitdiff \| tree
2020-01-07	Andrew Reynolds	Fix unary minus parse check (#3594)	commit \| commitdiff \| tree
2020-01-07	Andrew Reynolds	Update any-constant and normalization policies for...	commit \| commitdiff \| tree
2019-12-31	Alex Ozdemir	[proof] ITE translation fix (#3484)	commit \| commitdiff \| tree
2019-12-19	Mathias Preiner	Fix typo in smt_options.toml. (#3579)	commit \| commitdiff \| tree
2019-12-18	Andrew Reynolds	Increment Taylor degree for tangent and secant plane...	commit \| commitdiff \| tree
2019-12-18	Andres Noetzli	Avoid calling rewriter from type checker (#3548)	commit \| commitdiff \| tree
2019-12-17	Mathias Preiner	Generate code for options with modes. (#3561)	commit \| commitdiff \| tree
2019-12-16	Andrew Reynolds	Revert evaluate as node. (#3574)	commit \| commitdiff \| tree
2019-12-13	Andrew Reynolds	Eliminate Expr-level calls in TypeNode (#3562)	commit \| commitdiff \| tree
2019-12-13	Andrew Reynolds	Add support for set comprehension (#3312)	commit \| commitdiff \| tree
2019-12-12	Andrew Reynolds	Make CEGIS sampling robust to non-vanilla CEGIS (#3559)	commit \| commitdiff \| tree
2019-12-12	Andrew Reynolds	Use the node-level datatypes API (#3556)	commit \| commitdiff \| tree
2019-12-12	Andrew Reynolds	Fixes for regressions (#3557)	commit \| commitdiff \| tree
2019-12-12	Andrew Reynolds	Fix CEGIS refinement for recursive functions evaluation...	commit \| commitdiff \| tree
2019-12-12	Andrew Reynolds	Activate node-level datatype API (#3540)	commit \| commitdiff \| tree
2019-12-11	Andrew Reynolds	Do not substitute beneath arithmetic terms in the non...	commit \| commitdiff \| tree
2019-12-11	Andrew Reynolds	Support symbolic unfolding in UNIF+PI (#3553)	commit \| commitdiff \| tree
2019-12-10	Andrew Reynolds	Incorporate rewriting on demand in the evaluator (...	commit \| commitdiff \| tree
2019-12-10	Andrew Reynolds	Allow unsat cores with sygus inference (#3550)	commit \| commitdiff \| tree
2019-12-09	Andrew Reynolds	Disable sygus inference when combined with incremental...	commit \| commitdiff \| tree
2019-12-09	Andres Noetzli	Make theory rewriters non-static (#3547)	commit \| commitdiff \| tree
2019-12-07	Andres Noetzli	Use str.subtr in str.to.int/int.to.str reduction (...	commit \| commitdiff \| tree
2019-12-06	Andrew Reynolds	Throw exception instead of warning for approximate...	commit \| commitdiff \| tree
2019-12-06	Andres Noetzli	Add lemma for str.to.int/int.to.str (#3541)	commit \| commitdiff \| tree
2019-12-06	Andrew Reynolds	New algorithm for interpolation and abduction based...	commit \| commitdiff \| tree
2019-12-06	Andrew Reynolds	Add 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-05	Andrew Reynolds	Make nonlinear solver intercept model assignments from...	commit \| commitdiff \| tree
2019-12-05	Andrew Reynolds	Refactor mode options for Unif+PI (#3531)	commit \| commitdiff \| tree
2019-12-04	Andrew Reynolds	New grammar construction modes for SyGuS (#3486)	commit \| commitdiff \| tree
2019-12-04	Andrew Reynolds	Fix (#3530)	commit \| commitdiff \| tree
2019-12-04	Andrew Reynolds	Fixes for SyGuS PBE + templated string concatenations...	commit \| commitdiff \| tree
2019-12-04	Andrew Reynolds	Fix single invocation solution construction for multiple...	commit \| commitdiff \| tree
2019-12-04	Andres Noetzli	Fix corner case in model construction of strings (...	commit \| commitdiff \| tree
2019-12-03	Andrew Reynolds	Improve flexibility of lemma output in non-linear solver...	commit \| commitdiff \| tree
2019-12-03	Aina Niemetz	Fix clang-format file for brace wrapping with case...	commit \| commitdiff \| tree
2019-12-03	makaimann	Minor refactor: rename opterm_black to op_black (#3521)	commit \| commitdiff \| tree
2019-12-02	makaimann	OpTerm Refactor: Allow retrieving OpTerm used to create...	commit \| commitdiff \| tree
2019-12-02	Andrew Reynolds	Update ownership policy for dynamic quantifiers splitting...	commit \| commitdiff \| tree
2019-12-02	Andrew Reynolds	Fix case of higher-order + sygus inference (#3509)	commit \| commitdiff \| tree
2019-12-02	Andrew Reynolds	Ensure quantifiers options are set with --no-strings...	commit \| commitdiff \| tree
2019-11-30	Andrew Reynolds	Fix fast SyGuS enumeration for interpreted constants...	commit \| commitdiff \| tree
2019-11-29	Andrew Reynolds	Check free variables in assertions when using SyGuS...	commit \| commitdiff \| tree
2019-11-27	Andrew Reynolds	Fix sygus inference for choice functions introduced...	commit \| commitdiff \| tree
2019-11-27	Haniel Barbosa	Enable sygusRecFun by default and fixes SyGuS+RecFun...	commit \| commitdiff \| tree
2019-11-27	Andrew Reynolds	Fix indexof range lemma (#3499)	commit \| commitdiff \| tree
2019-11-21	Haniel Barbosa	hard limit for rec-fun eval (#3485)	commit \| commitdiff \| tree
next

RSS Atom