summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2021-10-20Unify abstract values and uninterpreted constantsabstractValsAndres Noetzli
2021-10-20Make proofs of rewrites robust to use in internal subsolvers (#7411)Andrew Reynolds
2021-10-20Add basic regular expression type enumerator (#7416)Andrew Reynolds
2021-10-19Support sequences of fixed finite cardinality (#7371)Andrew Reynolds
2021-10-19Fix issue related to sanity checking integer models (#7363)Andrew Reynolds
2021-10-18Move check for experimental arrays features to `theory_arrays.cpp`. (#7391)Abdalrhman Mohamed
2021-10-15Fix issues related to proofs of lemmas with duplicate conclusions in strings ...Andrew Reynolds
2021-10-14Split entailment check from term database (#7342)Andrew Reynolds
2021-10-14Fix quantifiers variable elimination for parametric datatypes (#7358)Andrew Reynolds
2021-10-13Eliminate uses of rewrite from datatypes theory (#7354)Andrew Reynolds
2021-10-13Make (proof) equality engine use Env (#7336)Andrew Reynolds
2021-10-12Simplify refinement in sygus solver (#7343)Andrew Reynolds
2021-10-12Eliminate calls to currentResourceManager (#7350)Andrew Reynolds
2021-10-12Clean up occurrences of SmtEngine in comments. (#7349)Aina Niemetz
2021-10-12Minor cleaning of instantiation utilities (#7334)Andrew Reynolds
2021-10-12Simplify skolemization in sygus solver (#7331)Andrew Reynolds
2021-10-12fix deprecation of std::iterator (#7332)Ouyancheng
2021-10-11Rename SmtScope to SolverEngineScope. (#7284)Aina Niemetz
2021-10-09Remove static accesses to options where EnvObj is used (#7330)Gereon Kremer
2021-10-07Use skolem lemma in prop layer interfaces (#7320)Andrew Reynolds
2021-10-07Make the cardinality of the alphabet of strings configurable (#7298)Andrew Reynolds
2021-10-07Miscellaneous fixes from proof-new (#7313)Andrew Reynolds
2021-10-07Fast exit for string extended equality rewriter (#7312)Andrew Reynolds
2021-10-06Eliminate more hard coded uses of user context (#7309)Andrew Reynolds
2021-10-05First round of refactoring on NlModel (#7255)Gereon Kremer
2021-10-04Refactor internally generated bounded quantified formulas (#7291)Andrew Reynolds
2021-10-04Move isFiniteType from theory engine to Env (#7287)Andrew Reynolds
2021-10-04Eliminating static calls to rewriter in quantifiers (#7301)Andrew Reynolds
2021-10-04Eliminating static calls to rewriter from strings (#7302)Andrew Reynolds
2021-10-01Update theory preprocessor to use Env (#7288)Andrew Reynolds
2021-10-01Make preregistration safe for uninterpreted constants (#7292)Andrew Reynolds
2021-10-01Use the proper evaluator for optimized SyGuS datatype rewriting (#7266)Andrew Reynolds
2021-09-30Rename SmtEngine to SolverEngine. (#7282)Aina Niemetz
2021-09-30Rename files smt_engine.(cpp|h) to solver_engine.(cpp|h). (#7279)Aina Niemetz
2021-09-30bv: Refactor ppRewrite and move to TheoryBV. (#7271)Mathias Preiner
2021-09-30Make theory engine modules use Env (#7277)Andrew Reynolds
2021-09-30Simplify the syntax and representation of the separation logic empty heap con...Andrew Reynolds
2021-09-30Remove usage of static options in arithmetic theory (#7221)Gereon Kremer
2021-09-29Remove support for extended `(check-sat <term>)` command. (#7270)Abdalrhman Mohamed
2021-09-29Properly restrict PBE symmetry breaking for abduction queries (#7269)Andrew Reynolds
2021-09-29Add the strings array solver (#7232)Andrew Reynolds
2021-09-24Eliminate calls to Rewriter::rewrite from strings entailment checks (#7203)Andrew Reynolds
2021-09-23Generalize string enumerator for fixed length sequences (#7234)Andrew Reynolds
2021-09-23Eliminate Output macro in favor of simple Env functions (#7223)Gereon Kremer
2021-09-23[proofs] Alethe: Translate THEORY_REWRITE (#7236)Lachnitt
2021-09-23Refactor check interface of nonlinear extension (#7235)Gereon Kremer
2021-09-23More uses of EnvObj (#7230)Andrew Reynolds
2021-09-23Use `|` to print quoted strings in `set-info` command. (#7240)Abdalrhman Mohamed
2021-09-23Implement alpha equivalence proofs (#7066)Andrew Reynolds
2021-09-22Make cegqi subsolvers EnvObj (#7205)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback