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

2020-02-18	Andrew Reynolds	Add missing kinds for the new API (#3757)	commit \| commitdiff \| tree
2020-02-17	Andrew Reynolds	Option to limit the number of rounds of enumerative...	commit \| commitdiff \| tree
2020-02-17	Andrew Reynolds	Fix soundness bug in reduction of integer div/mod... ...introduced 7 years ago in https://github.com/CVC4/CVC4/commit/9098391fe334d829ec...	commit \| commitdiff \| tree
2020-02-17	Haniel Barbosa	Using ParseOp in TPTP (#3764)	commit \| commitdiff \| tree
2020-02-17	Abdalrhman Mohamed	Support dumping Sygus commands. (#3763)	commit \| commitdiff \| tree
2020-02-16	Andrew Reynolds	Fix simple issue with cache (#3762)	commit \| commitdiff \| tree
2020-02-16	Andrew Reynolds	Add temporary global API conversion utilities. (#3759)	commit \| commitdiff \| tree
2020-02-16	Andres Noetzli	Activate reverse variant of F-Split inference (#3745)	commit \| commitdiff \| tree
2020-02-16	Andrew Reynolds	Disable regression (#3761)	commit \| commitdiff \| tree
2020-02-15	Andrew Reynolds	Move proxy variables to InferenceManager in strings...	commit \| commitdiff \| tree
2020-02-14	Andrew Reynolds	Remove quantifiers rewrite rules infrastructure (#3754)	commit \| commitdiff \| tree
2020-02-14	Andrew Reynolds	Update sygus v1 parser to use ParseOp utility (#3756)	commit \| commitdiff \| tree
2020-02-14	Haniel Barbosa	Forcing rewrite pass rather than asserting if formula...	commit \| commitdiff \| tree
2020-02-13	Andrew Reynolds	Const input for sygus print callback (#3755)	commit \| commitdiff \| tree
2020-02-13	Andres Noetzli	[Python] Properly destroy CVC4 object (#3753)	commit \| commitdiff \| tree
2020-02-12	Andres Noetzli	Rename Java package to edu.stanford.CVC4 (#3752)	commit \| commitdiff \| tree
2020-02-12	Andrew Reynolds	Ensure ext rewrites for associative ops dont throw...	commit \| commitdiff \| tree
2020-02-12	Mathias Preiner	run_regression: Distinguish between timeout and failure...	commit \| commitdiff \| tree
2020-02-12	Andrew Reynolds	Fix non-linear equality solving that involves mixed... ...43099566+ahmed-irfan@users.noreply.github.com>	commit \| commitdiff \| tree
2020-02-11	Mathias Preiner	cmake: Remove unused ENABLE_OPTIMIZED option. (#3749)	commit \| commitdiff \| tree
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) ...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
next

RSS Atom