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

2020-03-26	Andrew Reynolds	Generalize more string-specific functions (#4152)	commit \| commitdiff \| tree
2020-03-26	Andrew Reynolds	Care graphs based on polymorphic operators in strings...	commit \| commitdiff \| tree
2020-03-25	Andrew Reynolds	Generalize more uses of string-specific functions...	commit \| commitdiff \| tree
2020-03-24	Andrew Reynolds	Restrict partial triggers to standard quantified formulas...	commit \| commitdiff \| tree
2020-03-24	Andrew Reynolds	Restrict cases of sygus grammar reduction based on...	commit \| commitdiff \| tree
2020-03-23	Andrew Reynolds	Infer when sygus operators are equivalent to builtin...	commit \| commitdiff \| tree
2020-03-23	Andrew Reynolds	Simplify auxiliary variable handling in CEGQI (#4141)	commit \| commitdiff \| tree
2020-03-23	Andrew Reynolds	Throw exception for non-well-founded unimplemented...	commit \| commitdiff \| tree
2020-03-23	Andrew Reynolds	Change transcendental function app slave list to unordered_s...	commit \| commitdiff \| tree
2020-03-22	Andrew Reynolds	Sort inference does not handle APPLY_UF when higher...	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Generalize mkConcat for types (#4123)	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Fix variable shadowing issue in sygus-inference (#4121)	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Fix sort comparison within assertion in cegis (#4113)	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Guard cases of sort inference in quantifier free logics...	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Split string-specific operators from TheoryStringsRewriter...	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Do not assign higher-order representative if function...	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Handle failures for sygus QE preprocess (#4072)	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Parse error for SyGuS version 1.0 vs 2.0 (#4057)	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Make handling of illegal internal representatives in...	commit \| commitdiff \| tree
2020-03-20	Andrew Reynolds	Refactor enumerator for strings (#4014)	commit \| commitdiff \| tree
2020-03-19	Andrew Reynolds	Fix regression output related to sygus+bv-div-zero...	commit \| commitdiff \| tree
2020-03-19	Andrew Reynolds	SyGuS must use total bitvector division (#4119)	commit \| commitdiff \| tree
2020-03-19	Andrew Reynolds	Remove spurious assertion (#4117)	commit \| commitdiff \| tree
2020-03-19	Andrew Reynolds	Explicitly handle isFinite for rounding modes (#4115)	commit \| commitdiff \| tree
2020-03-19	Andrew Reynolds	Always enable cbqi literal dependency (#4116)	commit \| commitdiff \| tree
2020-03-19	Andrew Reynolds	Fix issue with multiple infinities in CEGQI for LIRA...	commit \| commitdiff \| tree
2020-03-16	Andrew Reynolds	Handle cases in --sygus-rr where evaluation is not...	commit \| commitdiff \| tree
2020-03-13	Andrew Reynolds	Removing a few deprecated options (#4052)	commit \| commitdiff \| tree
2020-03-13	Andrew Reynolds	Remove regress for real to int (#4071)	commit \| commitdiff \| tree
2020-03-13	Andrew Reynolds	Generalize type rules for strings to sequences (#3987)	commit \| commitdiff \| tree
2020-03-13	Andrew Reynolds	Fix case of non-constant value for sygus sampling ...	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Add options for nec regression (#4056)	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Convert most instances of dataypes in parsers to the...	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Do not allow quantifiers over real variables in real...	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Remove local theory extension option (#4048)	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Do not make models for quantified function variables...	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Ensure legal candidate equalities when using relational...	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Fix double notify in equality engine (#4036)	commit \| commitdiff \| tree
2020-03-12	Andrew Reynolds	Simplifications to the Datatypes API (#4040)	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Do not enable some SMT-COMP specific options by default...	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Guard against null relevancy condition in SyGuS (#4033)	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Add missing datatype functions to new API (#3930)	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Switch to Nodes for conjecture generator (#4026)	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Remove experimental symmetry breaker (#4005)	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Fix non-parametrized operators in subgoal generation...	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Remove partial instantiation for local theory extensions...	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Fix (#4017)	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Fix duplicate variable issue in sygus-qe-preproc (...	commit \| commitdiff \| tree
2020-03-11	Andrew Reynolds	Fix real to int for parameterized kinds (#4016)	commit \| commitdiff \| tree
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	Andrew Reynolds	Logic exception instead of assertion failure for instantiate...	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	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	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	Andrew Reynolds	Fix type issue in arith rewrite equality (#3972)	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	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-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	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-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-03	Andrew Reynolds	Standardize the interface for SMT engine subsolvers...	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	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	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	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
next

RSS Atom