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

2020-08-03	Andrew Reynolds	Split expression names from SmtEngine (#4832)	blob \| commitdiff \| raw
2020-08-03	Andrew Reynolds	Split dump manager from SmtEngine (#4824)	blob \| commitdiff \| raw \| diff to current
2020-07-31	Andrew Reynolds	Split listener classes from SmtEngine (#4816)	blob \| commitdiff \| raw \| diff to current
2020-07-28	Andres Noetzli	Replace Expr with Node in Term/Op (#4781)	blob \| commitdiff \| raw \| diff to current
2020-07-28	yoni206	Supporting seq.nth (#4723)	blob \| commitdiff \| raw \| diff to current
2020-07-17	Andrew Reynolds	Replace options listener infrastructure (#4764)	blob \| commitdiff \| raw \| diff to current
2020-07-16	Gereon Kremer	Resource manager cleanup (#4732)	blob \| commitdiff \| raw \| diff to current
2020-07-16	Andrew Reynolds	Split abstract values utility from SmtEngine (#4754)	blob \| commitdiff \| raw \| diff to current
2020-07-16	Gereon Kremer	Remove cumulative time limits and cpu time limits ...	blob \| commitdiff \| raw \| diff to current
2020-07-15	Andres Noetzli	Use Nodes for SmtEngine assertions (#4752)	blob \| commitdiff \| raw \| diff to current
2020-07-15	Andrew Reynolds	Split abduction solver from SmtEngine (#4733)	blob \| commitdiff \| raw \| diff to current
2020-07-14	Andrew Reynolds	Make use of options in setDefaults more consistent...	blob \| commitdiff \| raw \| diff to current
2020-07-07	Andrew Reynolds	Transfer ownership of internal Options from NodeManager...	blob \| commitdiff \| raw \| diff to current
2020-06-30	Ying Sheng	Interpolation step 1 (#4638)	blob \| commitdiff \| raw \| diff to current
2020-06-25	Andrew Reynolds	Remove sygus1 parser (#4651)	blob \| commitdiff \| raw \| diff to current
2020-06-19	Andres Noetzli	Add logic check for define-fun(s)-rec (#4577)	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-06-06	Andres Noetzli	Keep definitions when global-declarations enabled ...	blob \| commitdiff \| raw \| diff to current
2020-06-04	Aina Niemetz	New C++ Api: Second and last batch of API guards. ...	blob \| commitdiff \| raw \| diff to current
2020-05-20	Andrew Reynolds	Use debug-check-model to enable internal debugging...	blob \| commitdiff \| raw \| diff to current
2020-04-28	Andrew Reynolds	Support the SMT-LIB Unicode string standard by default...	blob \| commitdiff \| raw \| diff to current
2020-04-10	Andrew Reynolds	Towards proper use of resource managers (#4233)	blob \| commitdiff \| raw \| diff to current
2020-04-09	Andrew Reynolds	Split ProcessAssertions module from SmtEngine (#4210)	blob \| commitdiff \| raw \| diff to current
2020-04-08	Andres Noetzli	Perform theory widening eagerly (#4044)	blob \| commitdiff \| raw \| diff to current
2020-04-06	Andrew Reynolds	Remove links field in all toml files (#4201)	blob \| commitdiff \| raw \| diff to current
2020-04-03	Andres Noetzli	Update theory rewriter ownership, add stats to strings...	blob \| commitdiff \| raw \| diff to current
2020-04-01	Aina Niemetz	Rename checkValid/query to checkEntailed. (#4191)	blob \| commitdiff \| raw \| diff to current
2020-03-31	Andrew Reynolds	Remove replay and use-theory options and idl (#4186)	blob \| commitdiff \| raw \| diff to current
2020-03-27	Andres Noetzli	Fix issues with unsat cores and reset-assertions (...	blob \| commitdiff \| raw \| diff to current
2020-03-27	Andrew Reynolds	Move set defaults function to its own file (#4154)	blob \| commitdiff \| raw \| diff to current
2020-03-24	yoni206	Int2BV fail on demand (#4079)	blob \| commitdiff \| raw \| diff to current
2020-03-20	Andrew Reynolds	Handle failures for sygus QE preprocess (#4072)	blob \| commitdiff \| raw \| diff to current
2020-03-19	yoni206	Bv2int fail on demand	blob \| commitdiff \| raw \| diff to current
2020-03-19	Andrew Reynolds	SyGuS must use total bitvector division (#4119)	blob \| commitdiff \| raw \| diff to current
2020-03-18	Alex Ozdemir	Move node visitor class from smt_util/ to expr/ (#4110)	blob \| commitdiff \| raw \| diff to current
2020-03-17	Aina Niemetz	SmtEngine: Convert members owned by SmtEngine to unique...	blob \| commitdiff \| raw \| diff to current
2020-03-16	Andres Noetzli	Create master equality engine at context level 0 (...	blob \| commitdiff \| raw \| diff to current
2020-03-12	Andrew Reynolds	Remove local theory extension option (#4048)	blob \| commitdiff \| raw \| diff to current
2020-03-11	Andrew Reynolds	Do not enable some SMT-COMP specific options by default...	blob \| commitdiff \| raw \| diff to current
2020-03-11	Andres Noetzli	reset-assertions: Update TheoryEngine's PropEngine...	blob \| commitdiff \| raw \| diff to current
2020-03-11	Andrew Reynolds	Remove experimental symmetry breaker (#4005)	blob \| commitdiff \| raw \| diff to current
2020-03-10	Aina Niemetz	Fix issue with reset-assertions. (#3988)	blob \| commitdiff \| raw \| diff to current
2020-03-10	Andrew Reynolds	Consolidate options that disable produceModels (#3973)	blob \| commitdiff \| raw \| diff to current
2020-03-10	Andrew Reynolds	Rename sygus option name (#3977)	blob \| commitdiff \| raw \| diff to current
2020-03-06	Andrew Reynolds	Simplify DatatypeDeclarationCommand command (#3928)	blob \| commitdiff \| raw \| diff to current
2020-03-06	Andres Noetzli	Remove --apply-to-const preprocessing pass (#3919)	blob \| commitdiff \| raw \| diff to current
2020-03-05	Aina Niemetz	Move ownership of DecisionEngine into PropEngine. ...	blob \| commitdiff \| raw \| diff to current
2020-03-05	Aina Niemetz	Revert "Move ownership of DecisionEngine into PropEngin...	blob \| commitdiff \| raw \| diff to current
2020-03-05	Andrew Reynolds	Move ownership of DecisionEngine into PropEngine. ...	blob \| commitdiff \| raw \| diff to current
2020-03-05	Mathias Preiner	Enable -Wshadow and fix warnings. (#3909)	blob \| commitdiff \| raw \| diff to current
2020-02-29	Andrew Reynolds	Throw warning instead of error for non-constant values...	blob \| commitdiff \| raw \| diff to current
2020-02-26	Andrew Reynolds	More fixes for printing sygus commands (#3812)	blob \| commitdiff \| raw \| diff to current
2020-02-26	Andres Noetzli	Remove portfolio leftovers (#3821)	blob \| commitdiff \| raw \| diff to current
2020-02-25	yoni206	bv_to_int preprocessing pass	blob \| commitdiff \| raw \| diff to current
2020-02-24	Abdalrhman Mohamed	Fix bugs related to printing Sygus commands (#3804)	blob \| commitdiff \| raw \| diff to current
2020-02-20	Mathias Preiner	resource manager: Add statistic for every resource...	blob \| commitdiff \| raw \| diff to current
2020-02-17	Abdalrhman Mohamed	Support dumping Sygus commands. (#3763)	blob \| commitdiff \| raw \| diff to current
2020-02-14	Andrew Reynolds	Remove quantifiers rewrite rules infrastructure (#3754)	blob \| commitdiff \| raw \| diff to current
2020-02-14	Haniel Barbosa	Forcing rewrite pass rather than asserting if formula...	blob \| commitdiff \| raw \| diff to current
2020-02-08	Andres Noetzli	Make "unknown" non-critical for unsat cores check ...	blob \| commitdiff \| raw \| diff to current
2020-02-07	Andrew Reynolds	Refactor check-model handling in SmtEngine (#3723)	blob \| commitdiff \| raw \| diff to current
2020-02-06	Andrew Reynolds	Generalize containsQuantifiers to hasClosure (#3722)	blob \| commitdiff \| raw \| diff to current
2020-01-31	Andrew Reynolds	Allow PBE symmetry breaking with sygus stream (#3686)	blob \| commitdiff \| raw \| diff to current
2020-01-30	Andrew Reynolds	Weaken assertion for models with approximations (#3667)	blob \| commitdiff \| raw \| diff to current
2020-01-15	Aina Niemetz	New C++ API: Add nullary constructor for Result. (...	blob \| commitdiff \| raw \| diff to current
2019-12-17	Mathias Preiner	Generate code for options with modes. (#3561)	blob \| commitdiff \| raw \| diff to current
2019-12-16	Ying Sheng	Support ackermannization on uninterpreted sorts in...	blob \| commitdiff \| raw \| diff to current
2019-12-10	Andrew Reynolds	Allow unsat cores with sygus inference (#3550)	blob \| commitdiff \| raw \| diff to current
2019-12-09	Andrew Reynolds	Disable sygus inference when combined with incremental...	blob \| commitdiff \| raw \| diff to current
2019-12-06	Andrew Reynolds	Throw exception instead of warning for approximate...	blob \| commitdiff \| raw \| diff to current
2019-12-06	Andrew Reynolds	New algorithm for interpolation and abduction based...	blob \| commitdiff \| raw \| diff to current
2019-12-05	Andrew Reynolds	Refactor mode options for Unif+PI (#3531)	blob \| commitdiff \| raw \| diff to current
2019-12-02	makaimann	OpTerm Refactor: Allow retrieving OpTerm used to create...	blob \| commitdiff \| raw \| diff to current
2019-12-02	Andrew Reynolds	Ensure quantifiers options are set with --no-strings...	blob \| commitdiff \| raw \| diff to current
2019-11-29	Andrew Reynolds	Check free variables in assertions when using SyGuS...	blob \| commitdiff \| raw \| diff to current
2019-11-27	Haniel Barbosa	Enable sygusRecFun by default and fixes SyGuS+RecFun...	blob \| commitdiff \| raw \| diff to current
2019-11-13	Andrew Reynolds	Distinguish unknown status for model printing (#3454)	blob \| commitdiff \| raw \| diff to current
2019-11-04	Andrew Reynolds	Make check synth solution robust to auxiliary assertion...	blob \| commitdiff \| raw \| diff to current
2019-11-04	Andrew Reynolds	Make getSynthSolution return a Bool (#3306)	blob \| commitdiff \| raw \| diff to current
2019-10-30	Mathias Preiner	Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...	blob \| commitdiff \| raw \| diff to current
2019-10-14	Andrew Reynolds	Apply sygus repair constant techniques restricted to...	blob \| commitdiff \| raw \| diff to current
2019-10-08	Piotr Trojanek	pass parameters by reference where it affects performance	blob \| commitdiff \| raw \| diff to current
2019-10-08	Andres Noetzli	Disallow --proof and --incremental (#3332)	blob \| commitdiff \| raw \| diff to current
2019-10-08	Ying Sheng	Make ackermannization generally applicable rather than...	blob \| commitdiff \| raw \| diff to current
2019-10-03	yoni206	Disable proofs for unsupported logics (#3327)	blob \| commitdiff \| raw \| diff to current
2019-09-27	Andres Noetzli	Make substitution index context-independent (#2474)	blob \| commitdiff \| raw \| diff to current
2019-09-25	Andrew Reynolds	Return choice functions for approximate values in get...	blob \| commitdiff \| raw \| diff to current
2019-09-18	Andrew Reynolds	Decouple fmf-bound and finite-model-find (#3297)	blob \| commitdiff \| raw \| diff to current
2019-09-16	Andrew Reynolds	Return RecoverableModalException when model is not...	blob \| commitdiff \| raw \| diff to current
2019-09-12	Andrew Reynolds	Encapsulate synth engine (#3271)	blob \| commitdiff \| raw \| diff to current
2019-09-04	Andrew Reynolds	Towards incremental SyGuS in SMT engine (#3195)	blob \| commitdiff \| raw \| diff to current
2019-08-28	Andrew Reynolds	Removing comments related to issues (#3232)	blob \| commitdiff \| raw \| diff to current
2019-08-28	Andrew Reynolds	Fixes for get-abduct (#3229)	blob \| commitdiff \| raw \| diff to current
2019-08-14	Mathias Preiner	Remove option --continued-execution. (#3189)	blob \| commitdiff \| raw \| diff to current
2019-08-14	Andrew Reynolds	Call separate SMT engine for single invocation sygus...	blob \| commitdiff \| raw \| diff to current
2019-08-14	Aina Niemetz	SmtEngine: Reorganize class according to guidelines...	blob \| commitdiff \| raw \| diff to current
2019-08-13	Andrew Reynolds	Track sygus variable to term relationship via attribut...	blob \| commitdiff \| raw \| diff to current
2019-08-13	Andrew Reynolds	Implement check abduct feature (#3152)	blob \| commitdiff \| raw \| diff to current
2019-08-05	Andrew Reynolds	Remove forward declarations in quantifiers engine ...	blob \| commitdiff \| raw \| diff to current
2019-08-02	Andrew Reynolds	Flip the polarity of the argument of get-abduct (#3153)	blob \| commitdiff \| raw \| diff to current
next

RSS Atom