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

2020-02-07	Andrew Reynolds	Example evaluation cache utility (#3698)	commit \| commitdiff \| tree
2020-02-07	Andrew Reynolds	Fix exact sqrt (#3721) ...43099566+ahmed-irfan@users.noreply.github.com>	commit \| commitdiff \| tree
2020-02-06	Andrew Reynolds	Generalize containsQuantifiers to hasClosure (#3722)	commit \| commitdiff \| tree
2020-02-05	Andrew Reynolds	Fix QF_NIA smt comp script (#3715)	commit \| commitdiff \| tree
2020-02-04	mudathirmahgoub	Update INSTALL.md (#3714)	commit \| commitdiff \| tree
2020-02-04	Alex Ozdemir	Articulate proof-related debug statements in arith...	commit \| commitdiff \| tree
2020-02-04	Aina Niemetz	--fp-exp: Better warning message. (#3709)	commit \| commitdiff \| tree
2020-02-04	Mathias Preiner	Fix header installation on MacOS. (#3660)	commit \| commitdiff \| tree
2020-02-04	Andrew Reynolds	Split base solver from the theory of strings (#3680)	commit \| commitdiff \| tree
2020-02-04	Andres Noetzli	Revert semantic change from refactoring (#3711)	commit \| commitdiff \| tree
2020-02-04	Alex Ozdemir	Regression tests for arithmetic proofs. (#3701)	commit \| commitdiff \| tree
2020-02-04	Aina Niemetz	Increase regression test time limit to 1200s. (#3704)	commit \| commitdiff \| tree
2020-02-03	Clark Barrett	Fix corner case - might need to REWRITE_AGAIN (#3706)	commit \| commitdiff \| tree
2020-02-03	Andrew Reynolds	Utility function for getting component types (#3703)	commit \| commitdiff \| tree
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) ...yoni206 <yoni206@users.noreply.github.com> ...yoni206 <yoni206@users.noreply.github.com>	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 substitution in nl solver (#3638) ...43099566+ahmed-irfan@users.noreply.github.com>	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... ...yoni206 <yoni206@users.noreply.github.com> ...yoni206 <yoni206@users.noreply.github.com>	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) ...yoni206 <yoni206@users.noreply.github.com> ...yoni206 <yoni206@users.noreply.github.com>	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... ...yoni206 <yoni206@users.noreply.github.com>	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
next

RSS Atom