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

2018-10-11	Haniel Barbosa	Fix default setting of CegisUnif options (#2605)	blob \| commitdiff \| raw
2018-10-11	Andrew Reynolds	Synthesize rewrite rules from inputs (#2608)	blob \| commitdiff \| raw \| diff to current
2018-10-09	Aina Niemetz	Fix compiler warnings. (#2601)	blob \| commitdiff \| raw \| diff to current
2018-10-05	Andrew Reynolds	Update default options for sygus (#2586)	blob \| commitdiff \| raw \| diff to current
2018-10-01	Andres Noetzli	Fix dumping pre/post preprocessing passes (#2469)	blob \| commitdiff \| raw \| diff to current
2018-10-01	Andres Noetzli	Refactor preprocessing pass registration (#2468)	blob \| commitdiff \| raw \| diff to current
2018-09-18	Andrew Reynolds	Move and rename sygus solver classes (#2488)	blob \| commitdiff \| raw \| diff to current
2018-09-17	Andres Noetzli	Remove unnecessary tracing from preprocessing (#2472)	blob \| commitdiff \| raw \| diff to current
2018-09-15	Andres Noetzli	Refactor how assertions are added to decision engine...	blob \| commitdiff \| raw \| diff to current
2018-09-11	Andrew Reynolds	Support model cores via option --produce-model-cores...	blob \| commitdiff \| raw \| diff to current
2018-09-11	Aina Niemetz	Refactor non-clausal simplify preprocessing pass. ...	blob \| commitdiff \| raw \| diff to current
2018-09-05	Andrew Reynolds	Finer-grained inference of substitutions in incremental...	blob \| commitdiff \| raw \| diff to current
2018-09-04	Aina Niemetz	Transfer ownership of learned literals from SMT engine...	blob \| commitdiff \| raw \| diff to current
2018-09-04	Aina Niemetz	Fix merge mishap of #2359.	blob \| commitdiff \| raw \| diff to current
2018-08-30	Mathias Preiner	Refactor theory preprocess into preprocessing pass...	blob \| commitdiff \| raw \| diff to current
2018-08-29	Mathias Preiner	Refactor MipLibTrick preprocessing pass. (#2359)	blob \| commitdiff \| raw \| diff to current
2018-08-28	Aina Niemetz	Move flag needsFinish from SMT engine to circuit propag...	blob \| commitdiff \| raw \| diff to current
2018-08-26	Andres Noetzli	Refactor unconstrained simplification pass (#2374)	blob \| commitdiff \| raw \| diff to current
2018-08-25	yoni206	Refactor quantifier macros preprocessing pass (#1840)	blob \| commitdiff \| raw \| diff to current
2018-08-25	Haniel Barbosa	Refactor nlExtPurify preprocessing pass (#1963)	blob \| commitdiff \| raw \| diff to current
2018-08-24	Andrew Reynolds	Remove spurious disabling of cbqi-all (#2368)	blob \| commitdiff \| raw \| diff to current
2018-08-24	Andrew Reynolds	Do not print internally generated datatypes in externa...	blob \| commitdiff \| raw \| diff to current
2018-08-23	Haniel Barbosa	Makes the filename be set in the SMT engine by default...	blob \| commitdiff \| raw \| diff to current
2018-08-23	Aina Niemetz	Refactor ITE simplification preprocessing pass. (#2360)	blob \| commitdiff \| raw \| diff to current
2018-08-23	Andres Noetzli	Use "filename" instead of "name" in SmtEngine::setInfo...	blob \| commitdiff \| raw \| diff to current
2018-08-23	yoni206	global-negate preprocessing pass (#2317)	blob \| commitdiff \| raw \| diff to current
2018-08-21	Tim King	Removing unused bool members in command.cpp. Also initi...	blob \| commitdiff \| raw \| diff to current
2018-08-21	Mathias Preiner	Move d_realAssertionsEnd from SmtEnginePrivate to Asser...	blob \| commitdiff \| raw \| diff to current
2018-08-21	Andrew Reynolds	Use cbqi-full for sygus (#2346)	blob \| commitdiff \| raw \| diff to current
2018-08-20	Andrew Reynolds	Make sygus inference a preprocessing pass (#2334)	blob \| commitdiff \| raw \| diff to current
2018-08-17	Andrew Reynolds	Eliminate partial operators in sygus grammar normaliza...	blob \| commitdiff \| raw \| diff to current
2018-08-17	Mathias Preiner	Refactor eager atoms preprocessing pass. (#2318)	blob \| commitdiff \| raw \| diff to current
2018-08-17	Haniel Barbosa	cleaning unnecessary timers/dumps (#2327)	blob \| commitdiff \| raw \| diff to current
2018-08-17	Caleb Donovick	Make quantifiers-preprocess preprocessing pass (#2322)	blob \| commitdiff \| raw \| diff to current
2018-08-17	Andres Noetzli	Refactor IteRemoval preprocessing pass (#1793)	blob \| commitdiff \| raw \| diff to current
2018-08-16	Haniel Barbosa	Refactor extended rewriter preprocessing pass (#2324)	blob \| commitdiff \| raw \| diff to current
2018-08-16	Haniel Barbosa	Refactor apply2const (#2316)	blob \| commitdiff \| raw \| diff to current
2018-08-15	Andres Noetzli	Remove unused tuple classes (#2313)	blob \| commitdiff \| raw \| diff to current
2018-08-15	Andrew Reynolds	Make sort inference a preprocessing pass (#2309)	blob \| commitdiff \| raw \| diff to current
2018-08-15	Andres Noetzli	Fix dumping of get-unsat-assumptions (#2302)	blob \| commitdiff \| raw \| diff to current
2018-08-08	Andrew Reynolds	Do beta-reduction in expandDefinitions (#2286)	blob \| commitdiff \| raw \| diff to current
2018-08-07	Andrew Reynolds	Move sygus quantifier elimination step for non-ground...	blob \| commitdiff \| raw \| diff to current
2018-08-06	Andrew Reynolds	Fixes for sygus inference (#2238)	blob \| commitdiff \| raw \| diff to current
2018-08-02	Andrew Reynolds	Fix issues with printing parametric datatypes in smt2...	blob \| commitdiff \| raw \| diff to current
2018-08-01	ayveejay	Improvements and tests for the API around separation...	blob \| commitdiff \| raw \| diff to current
2018-07-31	Mathias Preiner	Fix option handler for lazy/bv-sat-solver combinations...	blob \| commitdiff \| raw \| diff to current
2018-07-30	Mathias Preiner	Add support for incremental eager bit-blasting. (#1838)	blob \| commitdiff \| raw \| diff to current
2018-07-27	Andrew Reynolds	Make check-synth robust for assertions that are not...	blob \| commitdiff \| raw \| diff to current
2018-07-26	yoni206	Disabling bvLazyRewriteExtf in the right place (#2214)	blob \| commitdiff \| raw \| diff to current
2018-07-25	ayveejay	Performing clang-format on the original change-set...	blob \| commitdiff \| raw \| diff to current
2018-07-24	ayveejay	Adding API access methods to get heap/nil expressions...	blob \| commitdiff \| raw \| diff to current
2018-07-23	Andrew Reynolds	Generalize symmetry detection for 1 symmetry variable...	blob \| commitdiff \| raw \| diff to current
2018-07-17	yoni206	Refactor sep-pre-skolem-emp preprocessing pass	blob \| commitdiff \| raw \| diff to current
2018-07-17	Andrew Reynolds	Do extended rewrite on results of quantifier eliminatio...	blob \| commitdiff \| raw \| diff to current
2018-07-11	Caleb Donovick	Move rewrite to pass (#2128)	blob \| commitdiff \| raw \| diff to current
2018-07-03	Andrew Reynolds	sygusComp2018: update sygus-related options setting...	blob \| commitdiff \| raw \| diff to current
2018-07-03	Andrew Reynolds	Remove miscellaneous dead and unused code from quantifi...	blob \| commitdiff \| raw \| diff to current
2018-07-02	Aina Niemetz	Refactor ApplySubsts preprocessing pass. (#2120)	blob \| commitdiff \| raw \| diff to current
2018-07-02	Caleb Donovick	Add missing include (#2127)	blob \| commitdiff \| raw \| diff to current
2018-06-27	Andrew Reynolds	Synthesize candidate-rewrites from standard inputs...	blob \| commitdiff \| raw \| diff to current
2018-06-26	Andrew Reynolds	Disable uf symmetry breaker in incremental mode (...	blob \| commitdiff \| raw \| diff to current
2018-06-13	Andres Noetzli	Disable unconstrainedSimp pass when proofs enabled...	blob \| commitdiff \| raw \| diff to current
2018-06-09	Andres Noetzli	Reset decisions at SAT level after solving (#2059)	blob \| commitdiff \| raw \| diff to current
2018-06-04	Andrew Reynolds	Enable cegqi (with model values) for floating point...	blob \| commitdiff \| raw \| diff to current
2018-05-30	Aina Niemetz	Ignore license key in set-info command. (#2021)	blob \| commitdiff \| raw \| diff to current
2018-05-30	Andrew Reynolds	Fixes for quantifiers + incremental (#2009)	blob \| commitdiff \| raw \| diff to current
2018-05-29	Andres Noetzli	Make user's SMT2 version override file version (#2004)	blob \| commitdiff \| raw \| diff to current
2018-05-29	Andrew Reynolds	Disable minisat elimination when nonlinear is enabled...	blob \| commitdiff \| raw \| diff to current
2018-05-23	Andrew Reynolds	Add notions of evaluated kinds in TheoryModel (#1947)	blob \| commitdiff \| raw \| diff to current
2018-05-23	Andres Noetzli	Set same options for proofs as for unsat cores (#1957)	blob \| commitdiff \| raw \| diff to current
2018-05-22	Andres Noetzli	Disable symmetry breaker for unsat cores (#1958)	blob \| commitdiff \| raw \| diff to current
2018-05-22	Andrew Reynolds	Make sygus infer find function definitions (#1951)	blob \| commitdiff \| raw \| diff to current
2018-05-16	yoni206	Refactor static learning preprocessing pass (#1857)	blob \| commitdiff \| raw \| diff to current
2018-05-15	Andrew Reynolds	Minor improvements to --nl-ext-purify (#1896)	blob \| commitdiff \| raw \| diff to current
2018-05-11	Aina Niemetz	Fix ackermannize preprocessing pass. (#1904)	blob \| commitdiff \| raw \| diff to current
2018-05-10	Andrew Reynolds	Sygus repair constants (#1812)	blob \| commitdiff \| raw \| diff to current
2018-05-10	Aina Niemetz	Refactored BVAckermann preprocessing pass. (#1889)	blob \| commitdiff \| raw \| diff to current
2018-05-09	Andrew Reynolds	Better option names for PBE (#1891)	blob \| commitdiff \| raw \| diff to current
2018-05-09	Andrew Reynolds	Make symmetry-breaker-exp into a preprocessing pass...	blob \| commitdiff \| raw \| diff to current
2018-05-09	PaulMeng	Add the symmetry breaker module (#1847)	blob \| commitdiff \| raw \| diff to current
2018-05-08	Mathias Preiner	Refactor bv-abstraction preprocessing pass. (#1860)	blob \| commitdiff \| raw \| diff to current
2018-05-08	Andrew Reynolds	Infrastructure for approximations in model output ...	blob \| commitdiff \| raw \| diff to current
2018-05-08	Aina Niemetz	Fix order of preprocessing pass registration. (#1887)	blob \| commitdiff \| raw \| diff to current
2018-05-04	Mathias Preiner	Refactor bv-intro-pow2 preprocessing pass. (#1851)	blob \| commitdiff \| raw \| diff to current
2018-05-03	Mathias Preiner	Fix redundant internalPush calls. (#1865)	blob \| commitdiff \| raw \| diff to current
2018-05-03	Andrew Reynolds	Option to interleave tangent plane inferences (#1833)	blob \| commitdiff \| raw \| diff to current
2018-05-03	Andrew Reynolds	Initial support for string standard in smt lib 2.6...	blob \| commitdiff \| raw \| diff to current
2018-04-30	Haniel Barbosa	Refactor real2int (#1813)	blob \| commitdiff \| raw \| diff to current
2018-04-30	Andrew Reynolds	Remove subsort symmetry breaking (#1807)	blob \| commitdiff \| raw \| diff to current
2018-04-25	yoni206	Refactor bv-to-bool and bool-to-bv preprocessing passes...	blob \| commitdiff \| raw \| diff to current
2018-04-25	Andrew Reynolds	Add benchmark requiring subgoal generation with inducti...	blob \| commitdiff \| raw \| diff to current
2018-04-20	yoni206	Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv...	blob \| commitdiff \| raw \| diff to current
2018-04-20	PaulMeng	Symmetry detection module (#1749)	blob \| commitdiff \| raw \| diff to current
2018-04-19	Andres Noetzli	Refactor pbRewrites preprocessing pass (#1767)	blob \| commitdiff \| raw \| diff to current
2018-04-14	yoni206	allowing --bool-to-bv without quantifiers (#1771)	blob \| commitdiff \| raw \| diff to current
2018-04-11	Aina Niemetz	Refactored BVGauss preprocessing pass. (#1766)	blob \| commitdiff \| raw \| diff to current
2018-04-10	Andrew Reynolds	Improve accuracy of stats for sygus sampler (#1755)	blob \| commitdiff \| raw \| diff to current
2018-04-10	Aina Niemetz	Fix dumping of benchmark in SmtEngine::checkSatisfiabil...	blob \| commitdiff \| raw \| diff to current
2018-04-05	Mathias Preiner	Add more general SignExtendUltConst rewriting. (#1385)	blob \| commitdiff \| raw \| diff to current
2018-04-04	Andres Noetzli	Refactor IntToBV preprocessing pass (#1716)	blob \| commitdiff \| raw \| diff to current
next

RSS Atom