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

2020-03-10	Andrew Reynolds	Fix options for regression: --sort-inference is incompatible...	commit \| commitdiff \| tree
2020-03-10	Andrew Reynolds	Fix sort inference for top-level Boolean variables...	commit \| commitdiff \| tree
2020-03-10	Aina Niemetz	Fix issue with reset-assertions. (#3988)	commit \| commitdiff \| tree
2020-03-10	Andrew Reynolds	Logic exception instead of assertion failure for instantiate...	commit \| commitdiff \| tree
2020-03-10	Mathias Preiner	Update bug report template	commit \| commitdiff \| tree
2020-03-10	Andrew Reynolds	Remove assertion in resolution bound inferences (#3980)	commit \| commitdiff \| tree
2020-03-10	Andrew Reynolds	Consolidate options that disable produceModels (#3973)	commit \| commitdiff \| tree
2020-03-10	Andrew Reynolds	Fix assertion failure in sort inference for Boolean...	commit \| commitdiff \| tree
2020-03-10	Aina Niemetz	Fix -Wshadow warnings in sygus_grammar_cons.cpp. (...	commit \| commitdiff \| tree
2020-03-10	Andrew Reynolds	Do not set values for non-linear mult terms in collectModelI...	commit \| commitdiff \| tree
2020-03-10	Andrew Reynolds	Fix real as int for incremental (#3979)	commit \| commitdiff \| tree
2020-03-10	Andrew Reynolds	Do not traverse quantifiers in nl ext purify (#3982)	commit \| commitdiff \| tree
2020-03-10	Andrew Reynolds	Only register sygus terms to unfold if option is set...	commit \| commitdiff \| tree
2020-03-10	Alex Ozdemir	Document bv-to-bool recursion (#3848)	commit \| commitdiff \| tree
2020-03-10	makaimann	Enhancement: make the bool-to-bv pass more robust and...	commit \| commitdiff \| tree
2020-03-10	Andrew Reynolds	Rename sygus option name (#3977)	commit \| commitdiff \| tree
2020-03-10	Andrew Reynolds	Remove instantiation propagator infrastructure (#3975)	commit \| commitdiff \| tree
2020-03-10	Andrew Reynolds	Ensure standard miniscoping is applied before aggressive...	commit \| commitdiff \| tree
2020-03-09	Andrew Reynolds	Eliminate spurious assertion (#3976)	commit \| commitdiff \| tree
2020-03-09	Aina Niemetz	DecisionEngine: Use unique_ptr for enabled strategies...	commit \| commitdiff \| tree
2020-03-09	Andrew Reynolds	Fix type issue in arith rewrite equality (#3972)	commit \| commitdiff \| tree
2020-03-09	Andres Noetzli	Make registration of unit clauses more robust (#3965)	commit \| commitdiff \| tree
2020-03-09	Andres Noetzli	Increase stack size for Windows builds to 100 MB (...	commit \| commitdiff \| tree
2020-03-09	Andrew Reynolds	Clean up more uses of ExprManager in parsers (#3932)	commit \| commitdiff \| tree
2020-03-09	Andrew Reynolds	Convert more uses of strings to words (#3921)	commit \| commitdiff \| tree
2020-03-09	Andres Noetzli	Fix quoting of options on Travis (#3981)	commit \| commitdiff \| tree
2020-03-09	Andrew Reynolds	Fixes for bounds on transcendental functions (#3832)	commit \| commitdiff \| tree
2020-03-09	Andrew Reynolds	Rewrite again full for DIV rewrite (#3945)	commit \| commitdiff \| tree
2020-03-08	Ying Sheng	Explicit end marker for models printed in the CVC language...	commit \| commitdiff \| tree
2020-03-06	Andrew Reynolds	Minor refactor for theory of sets (#3924)	commit \| commitdiff \| tree
2020-03-06	Andrew Reynolds	Simplify DatatypeDeclarationCommand command (#3928)	commit \| commitdiff \| tree
2020-03-06	Andrew Reynolds	Remove tester name from APIs (#3929)	commit \| commitdiff \| tree
2020-03-06	Andres Noetzli	Ignore model check warning in regression test (#3926)	commit \| commitdiff \| tree
2020-03-06	Andrew Reynolds	Make sygus datatype building independent of parser...	commit \| commitdiff \| tree
2020-03-06	Andrew Reynolds	Support default sygus grammar construction for sets...	commit \| commitdiff \| tree
2020-03-06	Andres Noetzli	Make output of regression script more readable (#3911)	commit \| commitdiff \| tree
2020-03-06	Andres Noetzli	Remove --apply-to-const preprocessing pass (#3919)	commit \| commitdiff \| tree
2020-03-05	Andres Noetzli	Add a new arith constraint proof rule: IntTightenAP...	commit \| commitdiff \| tree
2020-03-05	Andrew Reynolds	Migrate a majority of the functionality in parsers...	commit \| commitdiff \| tree
2020-03-05	Andrew Reynolds	Move ownership of DecisionEngine into PropEngine. ...	commit \| commitdiff \| tree
2020-03-05	Andrew Reynolds	Fix issues with real to int (#3918)	commit \| commitdiff \| tree
2020-03-05	Mathias Preiner	Enable -Wshadow and fix warnings. (#3909)	commit \| commitdiff \| tree
2020-03-03	mudathirmahgoub	Refactoring and cleaning the type enumerator for sets...	commit \| commitdiff \| tree
2020-03-03	Andrew Reynolds	Standardize the interface for SMT engine subsolvers...	commit \| commitdiff \| tree
2020-03-03	Andres Noetzli	Fix `TheorySetsPrive::eqNotifyPostMerge()` (#3901)	commit \| commitdiff \| tree
2020-03-03	Mathias Preiner	Fix variable shadowing bug in sets. (#3898)	commit \| commitdiff \| tree
2020-03-02	Andrew Reynolds	Split collect model info by types in strings (#3847)	commit \| commitdiff \| tree
2020-02-29	Andrew Reynolds	Convert more uses of string to word (#3834)	commit \| commitdiff \| tree
2020-02-29	Andrew Reynolds	Throw warning instead of error for non-constant values...	commit \| commitdiff \| tree
2020-02-29	Andres Noetzli	Add support for str.from_code (#3829)	commit \| commitdiff \| tree
2020-02-29	Aina Niemetz	propEngine: Reorder class declaration according to...	commit \| commitdiff \| tree
2020-02-29	Andrew Reynolds	Fix assertion related to assignability in the model...	commit \| commitdiff \| tree
2020-02-29	Andrew Reynolds	Replace conditional rewrite pass in quantifiers with...	commit \| commitdiff \| tree
2020-02-28	Andrew Reynolds	Use enum for quantifiers rewrite steps (#3840)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Refactor operator applications in the parser (#3831)	commit \| commitdiff \| tree
2020-02-27	Haniel Barbosa	Changing TPTP parser to accomodate new API (#3837)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Update purifySygusGTerm to the new API (#3830)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Fix large models for strings (#3835)	commit \| commitdiff \| tree
2020-02-27	Andres Noetzli	Fix -Wshadow warnings in common headers (#3826)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Add support for is_digit and regular expression difference...	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Disable regression that times out on debug (#3833)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Move fix for vacuous sygus types out of the parser...	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Initial work towards -Wshadow (#3817)	commit \| commitdiff \| tree
2020-02-27	Andrew Reynolds	Some initial work on using words (#3819)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Infrastructure for tautological literals in nonlinear...	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Use side effect utility for non-linear lemmas (#3780)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Fix regression (#3827)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	More fixes for printing sygus commands (#3812)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Basic support for regular expression complement (#3437)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Refactor type ascriptions in the parser (#3825)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Minor improvement to ParseOp (#3808)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Use default consts when not using any const during...	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Fix node arity issue in reduction of int2bv (#3777)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Move equivalence class info to its own file in strings...	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Support for witnessing choice in models (#3781)	commit \| commitdiff \| tree
2020-02-26	Andres Noetzli	Remove portfolio leftovers (#3821)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Minor cleaning of smt2 parser (#3823)	commit \| commitdiff \| tree
2020-02-26	Andrew Reynolds	Embed mkAssociative utilities within the API. (#3801)	commit \| commitdiff \| tree
2020-02-25	mudathirmahgoub	Sets & Relations Java example (#3816)	commit \| commitdiff \| tree
2020-02-25	mudathirmahgoub	Sets & Relations Java example (#3816)	commit \| commitdiff \| tree
2020-02-25	yoni206	remove redundant includes (#3815)	commit \| commitdiff \| tree
2020-02-25	yoni206	bv_to_int preprocessing pass	commit \| commitdiff \| tree
2020-02-24	Andrew Reynolds	Fixes for quantifiers documentation (#3811)	commit \| commitdiff \| tree
2020-02-24	Andrew Reynolds	Utilities for words (#3797)	commit \| commitdiff \| tree
2020-02-24	Andrew Reynolds	Convert parser input interface to api::Term (#3809)	commit \| commitdiff \| tree
2020-02-24	Abdalrhman Mohamed	Fix bugs related to printing Sygus commands (#3804)	commit \| commitdiff \| tree
2020-02-24	Andrew Reynolds	Add missing functions to new C++ API (#3769)	commit \| commitdiff \| tree
2020-02-24	Andres Noetzli	Make lambda rewriter more robust (#3806)	commit \| commitdiff \| tree
2020-02-23	Andrew Reynolds	Minor refactoring of equality notifications (#3798)	commit \| commitdiff \| tree
2020-02-22	Alex Ozdemir	RIP th_lra.plf (#3796)	commit \| commitdiff \| tree
2020-02-22	Andrew Reynolds	Move check memberships to reg exp solver (#3793)	commit \| commitdiff \| tree
2020-02-22	Andrew Reynolds	Move cardinality inference scheme to base solver in...	commit \| commitdiff \| tree
2020-02-22	makaimann	Dump boolean propagations and conflicts for decision...	commit \| commitdiff \| tree
2020-02-22	Alex Ozdemir	Switch to th_lira.plf (#3741)	commit \| commitdiff \| tree
2020-02-21	Aina Niemetz	New C++ API: Remove TOTAL kinds. (#3794)	commit \| commitdiff \| tree
2020-02-21	Andrew Reynolds	Simple changes towards unicode string standard (#3791)	commit \| commitdiff \| tree
2020-02-21	Andrew V. Jones	Adding checks to the validation of 'bv-sat-solver'...	commit \| commitdiff \| tree
2020-02-21	Andrew Reynolds	Split extended functions solver in strings (#3768)	commit \| commitdiff \| tree
2020-02-21	Alex Ozdemir	Remove IntReal tightening axioms from th_lira.plf ...	commit \| commitdiff \| tree
2020-02-20	Andrew Reynolds	Remove front-end support for Chain (#3767)	commit \| commitdiff \| tree
next

RSS Atom