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

2020-03-11	Andrew Reynolds	Remove experimental symmetry breaker (#4005)	blob \| commitdiff \| raw
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
2019-08-02	Andrew Reynolds	Enable sygus logic when produce-abducts is true (#3144)	blob \| commitdiff \| raw \| diff to current
2019-08-01	Andrew Reynolds	Regular expression intersection modes (#3134)	blob \| commitdiff \| raw \| diff to current
2019-07-30	Andrew Reynolds	Track solver execution mode (#3132)	blob \| commitdiff \| raw \| diff to current
2019-07-30	Haniel Barbosa	Code to activate hoelim preprocessing pass (#3129)	blob \| commitdiff \| raw \| diff to current
2019-07-29	Andrew Reynolds	Model blocker feature (#3112)	blob \| commitdiff \| raw \| diff to current
2019-07-29	Andrew Reynolds	Support get-abduct smt2 command (#3122)	blob \| commitdiff \| raw \| diff to current
2019-07-01	Andrew Reynolds	Support sygus version 2 format (#3066)	blob \| commitdiff \| raw \| diff to current
2019-06-21	Andres Noetzli	Fix and simplify handling of --force-logic (#3062)	blob \| commitdiff \| raw \| diff to current
2019-06-11	Andrew Reynolds	Fix spurious assertion in get-value (#3052)	blob \| commitdiff \| raw \| diff to current
2019-06-04	Andres Noetzli	Enable proof checking for QF_LRA benchmarks (#2928)	blob \| commitdiff \| raw \| diff to current
2019-06-04	Andres Noetzli	Add check that result matches benchmark status (#3028)	blob \| commitdiff \| raw \| diff to current
2019-04-30	Andrew Reynolds	Eliminate APPLY kind (#2976)	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2019-03-22	makaimann	Use empty vector instead of false in query with null...	blob \| commitdiff \| raw \| diff to current
2019-03-20	Andrew Reynolds	Sygus abduction feature (#2744)	blob \| commitdiff \| raw \| diff to current
2019-03-16	Andres Noetzli	Limit --solve-int-as-bv=X to QF_NIA/QF_LIA/QF_IDL ...	blob \| commitdiff \| raw \| diff to current
2019-03-14	makaimann	check for null assumption in query and replace with...	blob \| commitdiff \| raw \| diff to current
2019-03-13	Andres Noetzli	Add statistics for proof gen./checking time, size ...	blob \| commitdiff \| raw \| diff to current
2019-01-18	Andres Noetzli	Fix ABC build (#2808)	blob \| commitdiff \| raw \| diff to current
2019-01-15	Andres Noetzli	Strings: Add option to change loop process mode (#2794)	blob \| commitdiff \| raw \| diff to current
2018-12-11	Andrew Reynolds	Remove alternate versions of mbqi (#2742)	blob \| commitdiff \| raw \| diff to current
2018-12-10	makaimann	BoolToBV modes (off, ite, all) (#2530)	blob \| commitdiff \| raw \| diff to current
2018-12-06	Andres Noetzli	Fix use-after-free due to destruction order (#2739)	blob \| commitdiff \| raw \| diff to current
2018-11-29	Andrew Reynolds	Combine sygus stream with PBE (#2726)	blob \| commitdiff \| raw \| diff to current
2018-11-27	Andrew Reynolds	Lazy model construction in TheoryEngine (#2633)	blob \| commitdiff \| raw \| diff to current
2018-11-21	Andrew Reynolds	Quickly recognize when PBE conjectures are infeasible...	blob \| commitdiff \| raw \| diff to current
2018-11-15	Andrew Reynolds	Expand definitions prior to model core computation...	blob \| commitdiff \| raw \| diff to current
2018-10-31	Andres Noetzli	Record assumption info in AssertionPipeline (#2678)	blob \| commitdiff \| raw \| diff to current
2018-10-22	Andres Noetzli	Recover from wrong use of get-info :reason-unknown...	blob \| commitdiff \| raw \| diff to current
2018-10-20	Andrew Reynolds	Sygus streaming non-implied predicates (#2660)	blob \| commitdiff \| raw \| diff to current
2018-10-19	Andres Noetzli	Add OptionException handling during initialization...	blob \| commitdiff \| raw \| diff to current
2018-10-19	Andrew Reynolds	Non-implied mode for model cores (#2653)	blob \| commitdiff \| raw \| diff to current
2018-10-18	Haniel Barbosa	Introducing internal commands for SyGuS commands (...	blob \| commitdiff \| raw \| diff to current
2018-10-18	Andrew Reynolds	Sygus query generator (#2465)	blob \| commitdiff \| raw \| diff to current
2018-10-15	Andrew Reynolds	Delay initialization of theory engine (#2621)	blob \| commitdiff \| raw \| diff to current
2018-10-13	Andres Noetzli	Reset input language for ExprMiner subsolver (#2624)	blob \| commitdiff \| raw \| diff to current
2018-10-11	Haniel Barbosa	Fix default setting of CegisUnif options (#2605)	blob \| commitdiff \| raw \| diff to current
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
next

RSS Atom