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

2020-02-11	Andrew Reynolds	Fix term simplification based on entailment in quantifiers...	commit \| commitdiff \| tree
2020-02-11	Mathias Preiner	Update issue templates	commit \| commitdiff \| tree
2020-02-11	Andres Noetzli	Remove `--strings-binary-csp` option (#3743)	commit \| commitdiff \| tree
2020-02-11	Andres Noetzli	Refactor `CoreSolver::processSimpleNEq()` (#3736)	commit \| commitdiff \| tree
2020-02-11	Andrew Reynolds	Use example evaluation cache instead of sygus PBE ...	commit \| commitdiff \| tree
2020-02-11	Alex Ozdemir	Implement LFSCArithProof::equalityType. (#3740)	commit \| commitdiff \| tree
2020-02-10	Alex Ozdemir	Add function for tightening literals (#3732)	commit \| commitdiff \| tree
2020-02-10	Mathias Preiner	cmake: Use ld.gold if available for faster link times...	commit \| commitdiff \| tree
2020-02-10	Alex Ozdemir	Add more IntReal predicates (#3731)	commit \| commitdiff \| tree
2020-02-08	Andrew Reynolds	Fix rewrite rules sat regressions (#3734)	commit \| commitdiff \| tree
2020-02-08	Andres Noetzli	Make "unknown" non-critical for unsat cores check ...	commit \| commitdiff \| tree
2020-02-08	Andrew Reynolds	Split strings finite model finding strategy (#3727)	commit \| commitdiff \| tree
2020-02-08	Andrew Reynolds	Split core solver from the theory of strings (#3713)	commit \| commitdiff \| tree
2020-02-08	Andrew Reynolds	Interface for example evaluation cache utilities (...	commit \| commitdiff \| tree
2020-02-07	mudathirmahgoub	Univeset Cardinality constraints for infinite types...	commit \| commitdiff \| tree
2020-02-07	Andrew Reynolds	Refactor check-model handling in SmtEngine (#3723)	commit \| commitdiff \| tree
2020-02-07	Alex Ozdemir	Propagate expected types through UF arguments (#3717)	commit \| commitdiff \| tree
2020-02-07	Alex Ozdemir	Add `ArithProof::{printInteger,getLfscFunction}` (...	commit \| commitdiff \| tree
2020-02-07	Andrew Reynolds	Statistics for fast enumerator (#3699)	commit \| commitdiff \| tree
2020-02-07	Andrew Reynolds	Example evaluation cache utility (#3698)	commit \| commitdiff \| tree
2020-02-07	Andrew Reynolds	Fix exact sqrt (#3721)	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)	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
next

RSS Atom