summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2021-11-03Refactor skolem construction (#7561)Andrew Reynolds
2021-11-02Add printing methods for some commands. (#7557)Abdalrhman Mohamed
2021-11-02Fix setDefaults() for proofs with bitblast-internal. (#7552)Mathias Preiner
2021-11-02Make quant elimination robust to presence of other quantified formulas (#7551)Andrew Reynolds
2021-11-01bv: Remove layered solver. (#7455)Mathias Preiner
2021-11-01Replace more static options accesses (#7531)Gereon Kremer
2021-10-28Add a `define-fun` command for each `:named` term. (#7308)Abdalrhman Mohamed
2021-10-27Deterministic variables for RE elim (#7489)Andrew Reynolds
2021-10-26[proofs] Fix singleton check in MACRO_RES post-processing (#7498)Haniel Barbosa
2021-10-26[proofs] Fix and simplify CHAIN_RESOLUTION checker (#7492)Haniel Barbosa
2021-10-26Disable sygus-inst when incremental (#7485)Andrew Reynolds
2021-10-25Add new method for enumerating unsat queries with SyGuS (#7459)Andrew Reynolds
2021-10-25Fix support for global declarations (#7480)Andrew Reynolds
2021-10-25Remove HOL/fmf bound messages in set defaults (#7487)Andrew Reynolds
2021-10-25Add inference for count map (#7264)mudathirmahgoub
2021-10-22Remove options::X__name (#7414)Gereon Kremer
2021-10-22[proof] Fixing CHAIN_RESOLUTION checker (#7465)Haniel Barbosa
2021-10-22Remove `--uf-ho` option (#7463)Andrew Reynolds
2021-10-20Throw exception if checking model with separation logic heap (#7422)Andrew Reynolds
2021-10-20Eliminate last static calls to rewriter from smt layer (#7355)Andrew Reynolds
2021-10-20Avoid escaping `double-quotes` twice. (#7409)Abdalrhman Mohamed
2021-10-19Fix expected conclusion for EQ_RESOLVE when expanding MACRO_SR_PRED_TRANSFORM...Andrew Reynolds
2021-10-14Fix (get-info :authors) (#7373)Gereon Kremer
2021-10-13Eliminate uses of rewrite from datatypes theory (#7354)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-12Provide a non-traversal interface to term formula removal (#7328)Andrew Reynolds
2021-10-11Rename SmtEngineStatistics to SolverEngineStatistics. (#7339)Aina Niemetz
2021-10-11Rename SmtScope to SolverEngineScope. (#7284)Aina Niemetz
2021-10-11Connect the LFSC printer (#7323)Andrew Reynolds
2021-10-09Remove static accesses to options where EnvObj is used (#7330)Gereon Kremer
2021-10-08A few more miscellaneous uses of EnvObj (#7325)Andrew Reynolds
2021-10-07Move preprocessor to smt solver (#7321)Andrew Reynolds
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-07Eliminate more circular dependencies on solver engine (#7311)Andrew Reynolds
2021-10-06Change semantics of dumpUnsatCoresFull (#7314)Gereon Kremer
2021-10-05Finish refactoring on option handlers (#7295)Gereon Kremer
2021-10-04Move isFiniteType from theory engine to Env (#7287)Andrew Reynolds
2021-10-04Make decision engine use env (#7300)Andrew Reynolds
2021-10-01Update theory preprocessor to use Env (#7288)Andrew Reynolds
2021-10-01Add the print benchmark utility (#7196)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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback