summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
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-23Eliminate Output macro in favor of simple Env functions (#7223)Gereon Kremer
2021-09-23[proofs] Alethe: Add Alethe Files to be Compiled (#7241)Lachnitt
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-22Towards standard usage of evaluator (#7189)Andrew Reynolds
2021-09-17Use a single `NodeManager` per thread (#7204)Andres Noetzli
2021-09-14Add get-difficulty to the API (#7194)Andrew Reynolds
2021-09-14Support sygus version 2.1 command assume (#7081)Andrew Reynolds
2021-09-14Utilities in preparation for print benchmark utility (#7190)Andrew Reynolds
2021-09-14Add proof manager method to translate difficulty map (#7159)Andrew Reynolds
2021-09-14proofs: Properly track pre- and post-rewrites in bbAtom(). (#7147)Mathias Preiner
2021-09-14Reimplement `--dump=raw-benchmark` as `-o raw-benchmark` (#7191)Andrew Reynolds
2021-09-13Connect difficulty manager to TheoryEngine (#7161)Andrew Reynolds
2021-09-11Use StatisticsRegistry from Env (#7166)Gereon Kremer
2021-09-11checkModel: Extend documentation. (#7177)Aina Niemetz
2021-09-10bv: Use EnvObj::rewrite() and EnvObj::options() in NodeBitblaster. (#7172)Mathias Preiner
2021-09-10More refactoring of set defaults (#7160)Andrew Reynolds
2021-09-09Add difficulty post-processor (#7150)Andrew Reynolds
2021-09-09Disable shared selectors for quantified logics without SyGuS (#7156)Andrew Reynolds
2021-09-08Improve pre-skolemization, move quantifiers preprocess to own file (#7153)Andrew Reynolds
2021-09-08A couple of minor cleanups (#7141)Gereon Kremer
2021-09-08Towards standard usage of ExtendedRewriter (#7145)Andrew Reynolds
2021-09-08Add option for using bound inference for relevant assertions (#7152)Andrew Reynolds
2021-09-08Use rewriteViaMethod instead of accessing builtin proof checker (#7146)Andrew Reynolds
2021-09-07Refactoring of proof manager initialization (#7073)Andrew Reynolds
2021-09-07Refactoring and fixes of set defaults for quantifiers (#7120)Andrew Reynolds
2021-09-03EnvObj: Add options(), context(), userContext(). (#7137)Aina Niemetz
2021-09-03Eliminate backwards ref to SmtEngine from abduction and interpol solvers (#7133)Andrew Reynolds
2021-09-03theory: Have Theory and TheoryArith* derive from EnvObj. (#7128)Aina Niemetz
2021-09-02EnvObj: Restrict access. (#7121)Aina Niemetz
2021-09-02Remove options::getAll() (#7111)Gereon Kremer
2021-09-02Implement lazy proof checking modes (#7106)Andrew Reynolds
2021-09-02Enable sygus-inst for FP, NIA and NRA. (#7098)Aina Niemetz
2021-09-02Add class EnvObj. (#7113)Aina Niemetz
2021-09-01Print response to get-model using the API (#7084)Andrew Reynolds
2021-09-01Make driver::totalTime a TimerStat (#7089)Gereon Kremer
2021-09-01Lazy proof reconstruction for strings theory solver (#7096)Andrew Reynolds
2021-08-31bv: Remove dump=bv-rewrites. (#7099)Aina Niemetz
2021-08-30Further refactoring of set defaults for incompatibility methods (#7072)Andrew Reynolds
2021-08-30Refactor filename handling (#7088)Gereon Kremer
2021-08-27Expand definitions in sygus operators at the SMT level (#7077)Andrew Reynolds
2021-08-27Add missing methods to Solver API for models (#7052)Andrew Reynolds
2021-08-26Eliminate currentSmtEngine for subsolver calls (#7068)Andrew Reynolds
2021-08-26Dump models for isNotEntailed results (#7071)Andrew Reynolds
2021-08-26Consolidate language types (#7065)Gereon Kremer
2021-08-24Top-level structure for set defaults (#7047)Andrew Reynolds
2021-08-24Miscellaneous changes from proof-new (#7042)Andrew Reynolds
2021-08-20Make driver use options from the solver (#6930)Gereon Kremer
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback