summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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-12Get rid of unused member d_smtStats in ExpandDefs. (#7346)Aina Niemetz
2021-10-12Rename SmtEngineState to SolverEngineState. (#7344)Aina Niemetz
2021-10-12Fix glpk, add antlr.so (#7341)Gereon Kremer
2021-10-12Provide a non-traversal interface to term formula removal (#7328)Andrew Reynolds
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 SmtEngineStatistics to SolverEngineStatistics. (#7339)Aina Niemetz
2021-10-11Rename SmtScope to SolverEngineScope. (#7284)Aina Niemetz
2021-10-11Revert #7257 (#7337)Gereon Kremer
2021-10-11Connect the LFSC printer (#7323)Andrew Reynolds
2021-10-11Add cardinality constraint utilities (#7286)Andrew Reynolds
2021-10-11Restore compatibility with cmake 3.9 (#7329)Gereon Kremer
2021-10-09Remove static accesses to options where EnvObj is used (#7330)Gereon Kremer
2021-10-08Make skolem definition manager robust to function skolems (#7327)Andrew Reynolds
2021-10-08Add argument to distinguish lemmas and input assertions (#7326)Andrew Reynolds
2021-10-08A few more miscellaneous uses of EnvObj (#7325)Andrew Reynolds
2021-10-07Move preprocessor to smt solver (#7321)Andrew Reynolds
2021-10-07Finish the LFSC printer (#7285)Andrew Reynolds
2021-10-07Use skolem lemma in prop layer interfaces (#7320)Andrew Reynolds
2021-10-07Add new versioning scheme (#7253)Gereon Kremer
2021-10-07Make the cardinality of the alphabet of strings configurable (#7298)Andrew Reynolds
2021-10-07Add missing functions in Term.java (#7297)mudathirmahgoub
2021-10-07Fix/Improve static and shared builds with CLN or Poly (#7306)Gereon Kremer
2021-10-07Miscellaneous fixes from proof-new (#7313)Andrew Reynolds
2021-10-07Fast exit for string extended equality rewriter (#7312)Andrew Reynolds
2021-10-07Eliminate more circular dependencies on solver engine (#7311)Andrew Reynolds
2021-10-06Change behaviour of Term::getRealValue() (#7316)Gereon Kremer
2021-10-06Change semantics of dumpUnsatCoresFull (#7314)Gereon Kremer
2021-10-06Refactor skolem definitions notifications for the decision engine (#7310)Andrew Reynolds
2021-10-06Enable static builds in CI (#7281)Gereon Kremer
2021-10-06Eliminate more hard coded uses of user context (#7309)Andrew Reynolds
2021-10-06Avoid calling `quoteSymbol` multiple times. (#7307)Abdalrhman Mohamed
2021-10-05First round of refactoring on NlModel (#7255)Gereon Kremer
2021-10-05Finish refactoring on option handlers (#7295)Gereon Kremer
2021-10-04Add sygus examples to documentation (#7303)Gereon Kremer
2021-10-04Various improvements to documentation (#7283)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-04Make decision engine use env (#7300)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 java examples using the new Java API (#7225)mudathirmahgoub
2021-10-01Update theory preprocessor to use Env (#7288)Andrew Reynolds
2021-10-01Fix ascription check for return types on ordinary functions (#7290)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback