From f57d4b1b19342995fd5198c74d20c0254672043c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Oct 2012 11:28:03 -0700 Subject: [PATCH] reorganizing the code Signed-off-by: Leonardo de Moura --- scripts/mk_make.py | 3 +- scripts/mk_util.py | 13 + src/ast/normal_forms/nnf.cpp | 4 +- src/ast/pattern/database.smt2 | 332 ++++++++++++++++++ .../pattern}/expr_pattern_match.cpp | 21 +- src/{api => ast/pattern}/expr_pattern_match.h | 3 +- src/ast/pattern/pattern_inference.cpp | 13 +- src/ast/pattern/pattern_inference.h | 12 +- src/ast/rewriter/rewriter.h | 6 +- src/ast/rewriter/rewriter_def.h | 2 +- src/ast/rewriter/rewriter_types.h | 7 +- src/ast/rewriter/th_rewriter.cpp | 2 +- src/math/subpaving/subpaving_t_def.h | 5 +- src/model/model_evaluator.cpp | 2 +- src/muz_qe/qe_sat_tactic.cpp | 51 +-- src/nlsat/nlsat_solver.cpp | 6 +- src/sat/sat_solver.h | 4 +- src/sat/sat_types.h | 7 +- src/smt/asserted_formulas.cpp | 2 +- src/smt/asserted_formulas.h | 3 - src/tactic/arith/fix_dl_var_tactic.cpp | 7 +- src/tactic/arith/lia2pb_tactic.cpp | 7 +- src/tactic/arith/normalize_bounds_tactic.cpp | 7 +- src/tactic/arith/purify_arith_tactic.cpp | 37 +- src/tactic/arith/recover_01_tactic.cpp | 7 +- src/tactic/core/propagate_values_tactic.cpp | 7 +- src/tactic/core/simplify_tactic.cpp | 13 +- src/tactic/nlsat/nlsat_tactic.cpp | 1 + src/tactic/subpaving/subpaving_tactic.cpp | 20 +- src/tactic/tactic_exception.h | 41 +++ src/util/common_msgs.cpp | 26 ++ src/util/common_msgs.h | 39 ++ src/util/tactic_exception.cpp | 26 -- src/util/tactic_exception.h | 47 --- 34 files changed, 602 insertions(+), 181 deletions(-) create mode 100644 src/ast/pattern/database.smt2 rename src/{api => ast/pattern}/expr_pattern_match.cpp (97%) rename src/{api => ast/pattern}/expr_pattern_match.h (97%) create mode 100644 src/tactic/tactic_exception.h create mode 100644 src/util/common_msgs.cpp create mode 100644 src/util/common_msgs.h delete mode 100644 src/util/tactic_exception.cpp delete mode 100644 src/util/tactic_exception.h diff --git a/scripts/mk_make.py b/scripts/mk_make.py index da39fd709..419ffe221 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -30,9 +30,9 @@ add_lib('old_params', ['model', 'simplifier']) add_lib('cmd_context', ['tactic', 'rewriter', 'model', 'old_params', 'simplifier']) add_lib('substitution', ['ast'], 'ast/substitution') add_lib('normal_forms', ['rewriter', 'old_params'], 'ast/normal_forms') -add_lib('pattern', ['normal_forms'], 'ast/pattern') add_lib('parser_util', ['ast']) add_lib('smt2parser', ['cmd_context', 'parser_util']) +add_lib('pattern', ['normal_forms', 'smt2parser'], 'ast/pattern') add_lib('macros', ['simplifier', 'old_params'], 'ast/macros') add_lib('grobner', ['ast'], 'math/grobner') add_lib('euclid', ['util'], 'math/euclid') @@ -64,4 +64,5 @@ add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3') add_exe('test', ['api', 'fuzzing'], exe_name='test-z3') add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', dll_name='z3') +mk_auto_src() mk_makefile() diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 5817bb6bb..a3cc84832 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -414,4 +414,17 @@ def mk_makefile(): else: print "Type 'cd %s; make' to build Z3" % BUILD_DIR +# Generate automatically generated source code +def mk_auto_src(): + mk_pat_db() +# TODO: delete after src/ast/pattern/expr_pattern_match +# database.smt ==> database.h +def mk_pat_db(): + c = _Name2Component['pattern'] + fin = open('%s/database.smt2' % c.src_dir, 'r') + fout = open('%s/database.h' % c.src_dir, 'w') + fout.write('char const * g_pattern_database =\n') + for line in fin: + fout.write('"%s\\n"\n' % line.strip('\n')) + fout.write(';\n') diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index ec168a247..4d8849178 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -359,9 +359,9 @@ struct nnf::imp { void checkpoint() { cooperate("nnf"); if (memory::get_allocation_size() > m_max_memory) - throw nnf_exception(TACTIC_MAX_MEMORY_MSG); + throw nnf_exception(Z3_MAX_MEMORY_MSG); if (m_cancel) - throw nnf_exception(TACTIC_CANCELED_MSG); + throw nnf_exception(Z3_CANCELED_MSG); } void set_new_child_flag() { diff --git a/src/ast/pattern/database.smt2 b/src/ast/pattern/database.smt2 new file mode 100644 index 000000000..9021e44f0 --- /dev/null +++ b/src/ast/pattern/database.smt2 @@ -0,0 +1,332 @@ +(declare-fun ?store (Int Int Int) Int) +(declare-fun ?select (Int Int) Int) +(declare-fun ?PO (Int Int) Int) +(declare-fun ?asChild (Int Int) Int) +(declare-fun ?classDown (Int Int) Int) +(declare-fun ?array (Int) Int) +(declare-fun ?elemtype (Int) Int) +(declare-fun ?is (Int Int) Int) +(declare-fun ?cast (Int Int) Int) +(declare-fun ?Object () Int) +(declare-fun ?null () Int) +(declare-fun ?typeof (Int) Int) +(declare-fun ?asElems (Int) Int) +(declare-fun ?isAllocated (Int Int) Int) +(declare-fun ?fClosedTime (Int) Int) +(declare-fun ?eClosedTime (Int) Int) +(declare-fun ?max (Int) Int) +(declare-fun ?asLockSet (Int) Int) +(declare-fun ?isNewArray (Int) Int) +(declare-fun ?classLiteral (Int) Int) +(declare-fun ?Class () Int) +(declare-fun ?alloc () Int) +(declare-fun ?arrayType () Int) +(declare-fun ?f (Int) Int) +(declare-fun ?finv (Int) Int) +(declare-fun ?select2 (Int Int Int) Int) +(declare-fun ?store2 (Int Int Int Int) Int) +(declare-fun ?subtypes (Int Int) Bool) +(declare-fun ?Unbox (Int) Int) +(declare-fun ?UnboxedType (Int) Int) +(declare-fun ?Box (Int Int) Int) +(declare-fun ?System.Object () Int) +(declare-fun ?Smt.true () Int) +(declare-fun ?AsRepField (Int Int) Int) +(declare-fun ?AsPeerField (Int) Int) +(declare-fun ?nullObject () Int) +(declare-fun ?ownerRef_ () Int) +(declare-fun ?ownerFrame_ () Int) +(declare-fun IntsHeap (Int) Int) +(declare-fun ?localinv_ () Int) +(declare-fun ?inv_ () Int) +(declare-fun ?BaseClass_ (Int) Int) +(declare-fun ?typeof_ (Int) Int) +(declare-fun ?PeerGroupPlaceholder_ () Int) +(declare-fun ?ClassRepr (Int) Int) +(declare-fun ?RefArray (Int Int) Int) +(declare-fun Ints_ (Int Int) Int) +(declare-fun ?RefArrayGet (Int Int) Int) +(declare-fun ?elements_ () Int) +(declare-fun ?NonNullRefArray (Int Int) Int) +(declare-fun IntsNotNull_ (Int Int) Int) +(declare-fun ?Rank_ (Int) Int) +(declare-fun ?ValueArray (Int Int) Int) +(declare-fun ?ArrayCategory_ (Int) Int) +(declare-fun ?ArrayCategoryValue_ () Int) +(declare-fun ?ElementType_ (Int) Int) +(declare-fun ?System.Array () Int) +(declare-fun ?allocated_ () Int) +(declare-fun ?StructGet_ (Int Int) Int) +(declare-fun ?AsRangeField (Int Int) Int) +(declare-fun IntsAllocated (Int Int) Int) +(declare-fun IntnRange (Int Int) Bool) +(declare-fun ?isAllocated_ (Int Int) Bool) +(declare-fun ?AsDirectSubClass (Int Int) Int) +(declare-fun ?OneClassDown (Int Int) Int) +(assert (forall ((a Int) (i Int) (e Int)) + (! + (= (?select (?store a i e) i) e) + :pattern (?store a i e) + :weight 0))) +(assert (forall ((a Int) (i Int) (j Int) (e Int)) + (! + (or (= i j) (= (?select (?store a i e) j) (?select a j))) + :pattern (?select (?store a i e) j) + :weight 0))) +(assert (forall ((t0 Int) (t1 Int) (t2 Int)) + (! + (or (not (= (?PO t0 t1) 1)) + (not (= (?PO t1 t2) 1)) + (= (?PO t0 t2) 1)) + :pattern ((?PO t0 t1) (?PO t1 t2))))) +(assert (forall ((t0 Int) (t1 Int)) + (! + (or (not (= (?PO t0 t1) 1)) + (not (= (?PO t1 t0) 1)) + (= t0 t1)) + :pattern ((?PO t0 t1) (?PO t1 t0))))) +(assert (forall ((t0 Int) (t1 Int) (t2 Int)) + (! + (or (not (= (?PO t0 (?asChild t1 t2)) 1)) + (= (?classDown t2 t0) (?asChild t1 t2))) + :pattern (?PO t0 (?asChild t1 t2))))) +(assert (forall ((t Int)) + (! + (= (?finv (?f t)) t) + :pattern (?f t)))) +(assert (forall ((t0 Int) (t1 Int) ) + (! + (iff (= (?PO t0 (?array t1)) 1) + (not (or (not (= t0 (?array (?elemtype t0)))) + (not (= (?PO (?elemtype t0) t1) 1))))) + :pattern (?PO t0 (?array t1))))) +(assert (forall ((x Int) (t Int)) + (! + (or (not (= (?is x t) 1)) + (= (?cast x t) x)) + :pattern (?cast x t)))) +(assert (forall ((x Int) (t Int)) + (! + (or (not (= (?PO t ?Object) 1)) + (iff (= (?is x t) 1) + (or (= x ?null) + (= (?PO (?typeof x) t) 1)))) + :pattern ((?PO t ?Object) (?is x t))))) +(assert (forall ((e Int) (a Int) (i Int)) + (! + (= (?is (?select (?select (?asElems e) a) i) + (?elemtype (?typeof a))) 1) + :pattern (?select (?select (?asElems e) a) i)))) +(assert (forall ((x Int) (f Int) (a0 Int)) + (! + (or (<= (+ a0 (* -1 (?fClosedTime f))) 0) + (not (= (?isAllocated x a0) 1)) + (= (?isAllocated (?select f x) a0) 1)) + :pattern (?isAllocated (?select f x) a0)))) +(assert (forall ((a Int) (e Int) (i Int) (a0 Int)) + (! + (or (<= (+ a0 (* -1 (?eClosedTime e))) 0) + (not (= (?isAllocated a a0) 1)) + (= (?isAllocated (?select (?select e a) i) a0) 1)) + :pattern (?isAllocated (?select (?select e a) i) a0)))) +(assert (forall ((S Int)) + (! + (= (?select (?asLockSet S) (?max (?asLockSet S))) 1) + :pattern (?select (?asLockSet S) (?max (?asLockSet S)))))) +(assert (forall ((s Int)) + (! + (or (not (= 1 (?isNewArray s))) + (= (?PO (?typeof s) ?arrayType) 1)) + :pattern (?isNewArray s)))) +(assert (forall ((t Int)) + (! + (not (or (= (?classLiteral t) ?null) + (not (= (?is (?classLiteral t) ?Class) 1)) + (not (= (?isAllocated (?classLiteral t) ?alloc) 1)))) + :pattern (?classLiteral t)))) +(assert (forall ((A Int) (o Int) (f Int) (v Int)) + (! + (= (?select2 (?store2 A o f v) o f) v) + :pattern (?store2 A o f v) + :weight 0))) +(assert (forall ((A Int) (o Int) (f Int) (p Int) (g Int) (v Int)) + (! + (or (= o p) (= (?select2 (?store2 A o f v) p g) (?select2 A p g))) + :pattern (?select2 (?store2 A o f v) p g) + :weight 0))) +(assert (forall ((A Int) (o Int) (f Int) (p Int) (g Int) (v Int)) + (! + (or (= f g) (= (?select2 (?store2 A o f v) p g) (?select2 A p g))) + :pattern (?select2 (?store2 A o f v) p g) + :weight 0))) +(assert (forall ((t Int) (u Int) (v Int)) + (! + (or (not (?subtypes t u)) + (not (?subtypes u v)) + (?subtypes t v)) + :pattern ((?subtypes t u) (?subtypes u v))))) +(assert (forall ((t Int) (u Int)) + (! + (or (not (?subtypes t u)) + (not (?subtypes u t)) + (= t u)) + :pattern ((?subtypes t u) (?subtypes u t))))) +(assert (forall ((x Int) (p Int)) + (! + (or (not (?subtypes (?UnboxedType (?Box x p)) ?System.Object)) + (not (= (?Box x p) p)) + (= x p)) + :pattern (?subtypes (?UnboxedType (?Box x p)) ?System.Object)))) +(assert (forall ((h Int) (o Int) (f Int) (T Int)) + (! + (or + (not (= (IntsHeap h) ?Smt.true)) + (= (?select2 h o (?AsRepField f T)) ?nullObject) + (not (or (not (= (?select2 h (?select2 h o (?AsRepField f T)) ?ownerRef_) o)) + (not (= (?select2 h (?select2 h o (?AsRepField f T)) ?ownerFrame_) T))))) + :pattern (?select2 h o (?AsRepField f T))))) +(assert (forall ((h Int) (o Int) (f Int)) + (! + (or + (not (= (IntsHeap h) ?Smt.true)) + (= (?select2 h o (?AsPeerField f)) ?nullObject) + (not (or (not (= (?select2 h (?select2 h o (?AsPeerField f)) ?ownerRef_) (?select2 h o ?ownerRef_))) + (not (= (?select2 h (?select2 h o (?AsPeerField f)) ?ownerFrame_) (?select2 h o ?ownerFrame_)))))) + :pattern (?select2 h o (?AsPeerField f))))) +(assert (forall ((h Int) (o Int)) + (! + (or + (not (= (IntsHeap h) ?Smt.true)) + (= (?select2 h o ?ownerFrame_) ?PeerGroupPlaceholder_) + (not (?subtypes (?select2 h (?select2 h o ?ownerRef_) ?inv_) (?select2 h o ?ownerFrame_))) + (= (?select2 h (?select2 h o ?ownerRef_) ?localinv_) (?BaseClass_ (?select2 h o ?ownerFrame_))) + (not (or (not (= (?select2 h o ?inv_) (?typeof_ o))) + (not (= (?select2 h o ?localinv_) (?typeof_ o)))))) + :pattern (?subtypes (?select2 h (?select2 h o ?ownerRef_) ?inv_) (?select2 h o ?ownerFrame_))))) +(assert (forall ((T Int) (h Int)) + (! + (or (not (= (IntsHeap h) ?Smt.true)) + (= (?select2 h (?ClassRepr T) ?ownerFrame_) ?PeerGroupPlaceholder_)) + :pattern (?select2 h (?ClassRepr T) ?ownerFrame_)))) +(assert (forall ((a Int) (T Int) (i Int) (r Int) (heap Int)) + (! + (or (not (= (IntsHeap heap) ?Smt.true)) + (not (?subtypes (?typeof_ a) (?RefArray T r))) + (= (Ints_ (?RefArrayGet (?select2 heap a ?elements_) i) T) ?Smt.true)) + :pattern ((?subtypes (?typeof_ a) (?RefArray T r)) (?RefArrayGet (?select2 heap a ?elements_) i))))) +(assert (forall ((a Int) (T Int) (r Int)) + (! + (or (= a ?nullObject) + (not (?subtypes (?typeof_ a) (?RefArray T r))) + (= (?Rank_ a) r)) + :pattern (?subtypes (?typeof_ a) (?RefArray T r))))) +(assert (forall ((T Int) (ET Int) (r Int)) + (! + (or (not (?subtypes T (?ValueArray ET r))) + (= (?ArrayCategory_ T) ?ArrayCategoryValue_)) + :pattern (?subtypes T (?ValueArray ET r))))) +(assert (forall ((A Int) (r Int) (T Int)) + (! + (or + (not (?subtypes T (?RefArray A r))) + (not (or (not (= T (?RefArray (?ElementType_ T) r))) + (not (?subtypes (?ElementType_ T) A))))) + :pattern (?subtypes T (?RefArray A r))))) +(assert (forall ((A Int) (r Int) (T Int)) + (! + (or (not (?subtypes T (?ValueArray A r))) + (= T (?ValueArray A r))) + :pattern (?subtypes T (?ValueArray A r))))) +(assert (forall ((A Int) (B Int) (C Int)) + (! + (or (not (?subtypes C (?AsDirectSubClass B A))) + (= (?OneClassDown C A) B)) + :pattern (?subtypes C (?AsDirectSubClass B A))))) +(assert (forall ((o Int) (T Int)) + (! + (iff (= (Ints_ o T) ?Smt.true) + (or (= o ?nullObject) + (?subtypes (?typeof_ o) T))) + :pattern (Ints_ o T)))) +(assert (forall ((o Int) (T Int)) + (! + (iff (= (IntsNotNull_ o T) ?Smt.true) + (or (= o ?nullObject) + (not (= (Ints_ o T) ?Smt.true)))) + :pattern (IntsNotNull_ o T)))) +(assert (forall ((h Int) (o Int)) + (! + (or (not (= (IntsHeap h) ?Smt.true)) + (= o ?nullObject) + (not (?subtypes (?typeof_ o) ?System.Array)) + (not (or (not (= (?select2 h o ?inv_) (?typeof_ o))) + (not (= (?select2 h o ?localinv_) (?typeof_ o)))))) + :pattern ((?subtypes (?typeof_ o) ?System.Array) (?select2 h o ?inv_))))) +(assert (forall ((h Int) (o Int) (f Int) (T Int)) + (! + (or (not (= (IntsHeap h) ?Smt.true)) + (IntnRange (?select2 h o (?AsRangeField f T)) T)) + :pattern (?select2 h o (?AsRangeField f T))))) +(assert (forall ((h Int) (o Int) (f Int)) + (! + (or + (not (= (IntsHeap h) ?Smt.true)) + (not (= (?select2 h o ?allocated_) ?Smt.true)) + (= (IntsAllocated h (?select2 h o f)) ?Smt.true)) + :pattern (IntsAllocated h (?select2 h o f))))) +(assert (forall ((h Int) (s Int) (f Int)) + (! + (or (not (= (IntsAllocated h s) ?Smt.true)) + (= (IntsAllocated h (?StructGet_ s f)) ?Smt.true)) + :pattern (IntsAllocated h (?StructGet_ s f))))) +(assert (forall ((x Int) (f Int) (a0 Int)) + (! + (or (<= (+ a0 (* -1 (?fClosedTime f))) 0) + (not (?isAllocated_ x a0)) + (?isAllocated_ (?select f x) a0)) + :pattern (?isAllocated_ (?select f x) a0)))) +(assert (forall ((a Int) (e Int) (i Int) (a0 Int)) + (! + (or (<= (+ a0 (* -1 (?eClosedTime e))) 0) + (not (?isAllocated_ a a0)) + (?isAllocated_ (?select (?select e a) i) a0)) + :pattern (?isAllocated_ (?select (?select e a) i) a0)))) +(assert (forall ((e Int) (a Int) (i Int)) + (! + (= (?is (?select (?select (?asElems e) a) i) + (?elemtype (?typeof a))) ?Smt.true) + :pattern (?select (?select (?asElems e) a) i)))) +(assert (forall ((t0 Int) (t1 Int)) + (! + (iff (?subtypes t0 (?array t1)) + (not (or (not (= t0 (?array (?elemtype t0)))) + (not (?subtypes (?elemtype t0) t1))))) + :pattern (?subtypes t0 (?array t1))))) +(assert (forall ((t0 Int) (t1 Int) (t2 Int)) + (! + (or (not (?subtypes t0 (?asChild t1 t2))) + (= (?classDown t2 t0) (?asChild t1 t2))) + :pattern (?subtypes t0 (?asChild t1 t2))))) +(assert (forall ((t0 Int) (t1 Int)) + (! + (iff (?subtypes t0 (?array t1)) + (not (or (not (= t0 (?array (?elemtype t0)))) + (not (?subtypes (?elemtype t0) t1))))) + :pattern (?subtypes t0 (?array t1))))) +(assert (forall ((x Int) (t Int)) + (! + (or (not (= (?is x t) ?Smt.true)) + (= (?cast x t) x)) + :pattern (?cast x t)))) +(assert (forall ((x Int) (t Int)) + (! + (or (not (?subtypes t ?Object)) + (iff (= (?is x t) ?Smt.true) + (or (= x ?null) + (?subtypes (?typeof x) t)))) + :pattern ((?subtypes t ?Object) (?is x t))))) +(assert (forall ((e Int) (a Int) (i Int)) + (! + (= (?is (?select (?select (?asElems e) a) i) + (?elemtype (?typeof a))) 1) + :pattern (?select (?select (?asElems e) a) i)))) diff --git a/src/api/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp similarity index 97% rename from src/api/expr_pattern_match.cpp rename to src/ast/pattern/expr_pattern_match.cpp index e1698e043..3fe68c1ee 100644 --- a/src/api/expr_pattern_match.cpp +++ b/src/ast/pattern/expr_pattern_match.cpp @@ -31,10 +31,12 @@ Notes: #include"ast.h" #include"expr_pattern_match.h" -#include"smtparser.h" #include"for_each_ast.h" #include"ast_ll_pp.h" #include"ast_pp.h" +#include"cmd_context.h" +#include"smt2parser.h" +#include"front_end_params.h" expr_pattern_match::expr_pattern_match(ast_manager & manager): m_manager(manager), m_precompiled(manager) { @@ -398,21 +400,18 @@ expr_pattern_match::initialize(char const * spec_string) { if (!m_instrs.empty()) { return; } - m_instrs.push_back(instr(BACKTRACK)); - smtlib::parser* parser = smtlib::parser::create(m_manager); - parser->initialize_smtlib(); - if (!parser->parse_string(spec_string)) { - UNREACHABLE(); - } - smtlib::benchmark* bench = parser->get_benchmark(); - smtlib::theory::expr_iterator it = bench->begin_formulas(); - smtlib::theory::expr_iterator end = bench->end_formulas(); + std::istringstream is(spec_string); + front_end_params p; + cmd_context ctx(p, true, &m_manager); + VERIFY(parse_smt2_commands(ctx, is)); + + ptr_vector::const_iterator it = ctx.begin_assertions(); + ptr_vector::const_iterator end = ctx.end_assertions(); for (; it != end; ++it) { compile(*it); } - dealloc(parser); TRACE("expr_pattern_match", display(tout); ); } diff --git a/src/api/expr_pattern_match.h b/src/ast/pattern/expr_pattern_match.h similarity index 97% rename from src/api/expr_pattern_match.h rename to src/ast/pattern/expr_pattern_match.h index f0075b1ba..45295e627 100644 --- a/src/api/expr_pattern_match.h +++ b/src/ast/pattern/expr_pattern_match.h @@ -23,9 +23,8 @@ Notes: #include"ast.h" #include"map.h" #include"front_end_params.h" -#include"pattern_inference.h" -class expr_pattern_match : public pattern_database { +class expr_pattern_match { enum instr_kind { BACKTRACK, diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index 79cf41a71..773b9a2f5 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/src/ast/pattern/pattern_inference.cpp @@ -87,7 +87,7 @@ bool smaller_pattern::operator()(unsigned num_bindings, expr * p1, expr * p2) { return process(p1, p2); } -pattern_inference::pattern_inference(ast_manager & m, pattern_inference_params & params, pattern_database * db): +pattern_inference::pattern_inference(ast_manager & m, pattern_inference_params & params): simplifier(m), m_params(params), m_bfid(m.get_basic_family_id()), @@ -99,7 +99,7 @@ pattern_inference::pattern_inference(ast_manager & m, pattern_inference_params & m_pattern_weight_lt(m_candidates_info), m_collect(m, *this), m_contains_subpattern(*this), - m_database(db) { + m_database(m) { if (params.m_pi_arith == AP_NO) register_forbidden_family(m_afid); enable_ac_support(false); @@ -574,6 +574,8 @@ void pattern_inference::mk_patterns(unsigned num_bindings, m_candidates.reset(); } +#include"database.h" // defines g_pattern_database + void pattern_inference::reduce1_quantifier(quantifier * q) { TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m_manager) << "\n";); if (!q->is_forall()) { @@ -582,11 +584,12 @@ void pattern_inference::reduce1_quantifier(quantifier * q) { } int weight = q->get_weight(); - - if (m_database) { + + if (m_params.m_pi_use_database) { + m_database.initialize(g_pattern_database); app_ref_vector new_patterns(m_manager); unsigned new_weight; - if (m_database->match_quantifier(q, new_patterns, new_weight)) { + if (m_database.match_quantifier(q, new_patterns, new_weight)) { #ifdef Z3DEBUG for (unsigned i = 0; i < new_patterns.size(); i++) { SASSERT(is_well_sorted(m_manager, new_patterns.get(i))); } #endif diff --git a/src/ast/pattern/pattern_inference.h b/src/ast/pattern/pattern_inference.h index c477b0228..1a179e794 100644 --- a/src/ast/pattern/pattern_inference.h +++ b/src/ast/pattern/pattern_inference.h @@ -28,13 +28,7 @@ Revision History: #include"obj_hashtable.h" #include"obj_pair_hashtable.h" #include"map.h" - -class pattern_database { -public: - virtual ~pattern_database() {} - virtual void initialize(char const * smt_patterns) = 0; - virtual bool match_quantifier(quantifier * qf, app_ref_vector & patterns, unsigned & weight) = 0; -}; +#include"expr_pattern_match.h" /** \brief A pattern p_1 is smaller than a pattern p_2 iff @@ -195,7 +189,7 @@ class pattern_inference : public simplifier { }; ptr_vector m_pre_patterns; - pattern_database * m_database; + expr_pattern_match m_database; void candidates2unary_patterns(ptr_vector const & candidate_patterns, ptr_vector & remaining_candidate_patterns, @@ -223,7 +217,7 @@ class pattern_inference : public simplifier { virtual void reduce1_quantifier(quantifier * q); public: - pattern_inference(ast_manager & m, pattern_inference_params & params, pattern_database * db); + pattern_inference(ast_manager & m, pattern_inference_params & params); void register_forbidden_family(family_id fid) { SASSERT(fid != m_bfid); diff --git a/src/ast/rewriter/rewriter.h b/src/ast/rewriter/rewriter.h index a9b9bdb4f..f83277bdf 100644 --- a/src/ast/rewriter/rewriter.h +++ b/src/ast/rewriter/rewriter.h @@ -246,17 +246,17 @@ protected: // check maximum number of scopes void check_max_scopes() const { if (m_cfg.max_scopes_exceeded(this->m_scopes.size())) - throw rewriter_exception(TACTIC_MAX_SCOPES_MSG); + throw rewriter_exception(Z3_MAX_SCOPES_MSG); } // check maximum size of the frame stack void check_max_frames() const { if (m_cfg.max_frames_exceeded(frame_stack().size())) - throw rewriter_exception(TACTIC_MAX_FRAMES_MSG); + throw rewriter_exception(Z3_MAX_FRAMES_MSG); } // check maximum number of rewriting steps void check_max_steps() const { if (m_cfg.max_steps_exceeded(m_num_steps)) - throw rewriter_exception(TACTIC_MAX_STEPS_MSG); + throw rewriter_exception(Z3_MAX_STEPS_MSG); } // If pre_visit returns false, then t children are not visited/rewritten. diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 258a40a58..92f06679d 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -577,7 +577,7 @@ void rewriter_tpl::resume_core(expr_ref & result, proof_ref & result_pr) SASSERT(!frame_stack().empty()); while (!frame_stack().empty()) { if (m_cancel) - throw rewriter_exception(TACTIC_CANCELED_MSG); + throw rewriter_exception(Z3_CANCELED_MSG); SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size()); frame & fr = frame_stack().back(); expr * t = fr.m_curr; diff --git a/src/ast/rewriter/rewriter_types.h b/src/ast/rewriter/rewriter_types.h index e2164ef24..d42d6e2bc 100644 --- a/src/ast/rewriter/rewriter_types.h +++ b/src/ast/rewriter/rewriter_types.h @@ -19,7 +19,8 @@ Notes: #ifndef _REWRITER_TYPES_H_ #define _REWRITER_TYPES_H_ -#include"tactic_exception.h" +#include"z3_exception.h" +#include"common_msgs.h" /** \brief Builtin rewrite result status @@ -43,9 +44,9 @@ inline br_status unsigned2br_status(unsigned u) { return r; } -class rewriter_exception : public tactic_exception { +class rewriter_exception : public default_exception { public: - rewriter_exception(char const * msg):tactic_exception(msg) {} + rewriter_exception(char const * msg):default_exception(msg) {} }; #endif diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index a3f4b5e86..ee55d53e7 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -96,7 +96,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { bool max_steps_exceeded(unsigned num_steps) const { cooperate("simplifier"); if (memory::get_allocation_size() > m_max_memory) - throw rewriter_exception(TACTIC_MAX_MEMORY_MSG); + throw rewriter_exception(Z3_MAX_MEMORY_MSG); return num_steps > m_max_steps; } diff --git a/src/math/subpaving/subpaving_t_def.h b/src/math/subpaving/subpaving_t_def.h index 242fe088d..7c80de75c 100644 --- a/src/math/subpaving/subpaving_t_def.h +++ b/src/math/subpaving/subpaving_t_def.h @@ -20,7 +20,8 @@ Revision History: #include"interval_def.h" #include"buffer.h" #include"cooperate.h" -#include"tactic_exception.h" +#include"z3_exception.h" +#include"common_msgs.h" namespace subpaving { @@ -461,7 +462,7 @@ void context_t::checkpoint() { if (m_cancel) throw default_exception("canceled"); if (memory::get_allocation_size() > m_max_memory) - throw default_exception(TACTIC_MAX_MEMORY_MSG); + throw default_exception(Z3_MAX_MEMORY_MSG); cooperate("subpaving"); } diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 6519323ef..bccade304 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -193,7 +193,7 @@ struct evaluator_cfg : public default_rewriter_cfg { bool max_steps_exceeded(unsigned num_steps) const { cooperate("model evaluator"); if (memory::get_allocation_size() > m_max_memory) - throw rewriter_exception(TACTIC_MAX_MEMORY_MSG); + throw rewriter_exception(Z3_MAX_MEMORY_MSG); return num_steps > m_max_steps; } diff --git a/src/muz_qe/qe_sat_tactic.cpp b/src/muz_qe/qe_sat_tactic.cpp index 21a2a50ad..8cf5e5d58 100644 --- a/src/muz_qe/qe_sat_tactic.cpp +++ b/src/muz_qe/qe_sat_tactic.cpp @@ -250,31 +250,36 @@ namespace qe { proof_converter_ref & pc, expr_dependency_ref& core) { - checkpoint(); - reset(); - ptr_vector fmls; - goal->get_formulas(fmls); - m_fml = m.mk_and(fmls.size(), fmls.c_ptr()); - TRACE("qe", tout << "input: " << mk_pp(m_fml,m) << "\n";); - simplify_rewriter_star rw(m); - expr_ref tmp(m); - rw(m_fml, tmp); - m_fml = tmp; - TRACE("qe", tout << "reduced: " << mk_pp(m_fml,m) << "\n";); - skolemize_existential_prefix(); - extract_alt_form(m_fml); - model_ref model; - expr_ref res = qt(0, m.mk_true(), model); - goal->inc_depth(); - if (m.is_false(res)) { - goal->assert_expr(res); + try { + checkpoint(); + reset(); + ptr_vector fmls; + goal->get_formulas(fmls); + m_fml = m.mk_and(fmls.size(), fmls.c_ptr()); + TRACE("qe", tout << "input: " << mk_pp(m_fml,m) << "\n";); + simplify_rewriter_star rw(m); + expr_ref tmp(m); + rw(m_fml, tmp); + m_fml = tmp; + TRACE("qe", tout << "reduced: " << mk_pp(m_fml,m) << "\n";); + skolemize_existential_prefix(); + extract_alt_form(m_fml); + model_ref model; + expr_ref res = qt(0, m.mk_true(), model); + goal->inc_depth(); + if (m.is_false(res)) { + goal->assert_expr(res); + } + else { + goal->reset(); + // equi-satisfiable. What to do with model? + mc = model2model_converter(&*model); + } + result.push_back(goal.get()); } - else { - goal->reset(); - // equi-satisfiable. What to do with model? - mc = model2model_converter(&*model); + catch (rewriter_exception & ex) { + throw tactic_exception(ex.msg()); } - result.push_back(goal.get()); } virtual void collect_statistics(statistics & st) const { diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index b55a0a000..837e76ecd 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -25,7 +25,7 @@ Revision History: #include"nlsat_evaluator.h" #include"nlsat_explain.h" #include"algebraic_numbers.h" -#include"tactic_exception.h" +#include"z3_exception.h" #include"chashtable.h" #include"id_gen.h" #include"dependency.h" @@ -220,8 +220,8 @@ namespace nlsat { } void checkpoint() { - if (m_cancel) throw solver_exception(TACTIC_CANCELED_MSG); - if (memory::get_allocation_size() > m_max_memory) throw solver_exception(TACTIC_MAX_MEMORY_MSG); + if (m_cancel) throw solver_exception(Z3_CANCELED_MSG); + if (memory::get_allocation_size() > m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG); } // ----------------------- diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 378c070fa..2a64c9cd5 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -218,8 +218,8 @@ namespace sat { lbool status(clause const & c) const; clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); } void checkpoint() { - if (m_cancel) throw solver_exception(TACTIC_CANCELED_MSG); - if (memory::get_allocation_size() > m_config.m_max_memory) throw solver_exception(TACTIC_MAX_MEMORY_MSG); + if (m_cancel) throw solver_exception(Z3_CANCELED_MSG); + if (memory::get_allocation_size() > m_config.m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG); } protected: watch_list & get_wlist(literal l) { return m_watches[l.index()]; } diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 32a429dd5..db8de94a9 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -22,7 +22,8 @@ Revision History: #include"debug.h" #include"approx_set.h" #include"lbool.h" -#include"tactic_exception.h" +#include"z3_exception.h" +#include"common_msgs.h" #include"vector.h" #include @@ -125,9 +126,9 @@ namespace sat { class integrity_checker; typedef ptr_vector clause_vector; - class solver_exception : public tactic_exception { + class solver_exception : public default_exception { public: - solver_exception(char const * msg):tactic_exception(msg) {} + solver_exception(char const * msg):default_exception(msg) {} }; typedef default_exception sat_param_exception; diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index ab6d10019..368889cdc 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -1105,7 +1105,7 @@ void asserted_formulas::reduce_and_solve() { void asserted_formulas::infer_patterns() { IF_IVERBOSE(10, verbose_stream() << "pattern inference...\n";); TRACE("before_pattern_inference", display(tout);); - pattern_inference infer(m_manager, m_params, m_database.get()); + pattern_inference infer(m_manager, m_params); expr_ref_vector new_exprs(m_manager); proof_ref_vector new_prs(m_manager); unsigned i = m_asserted_qhead; diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index 62f3528c3..b08ac90d3 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -39,7 +39,6 @@ class bv_simplifier_plugin; class asserted_formulas { ast_manager & m_manager; front_end_params & m_params; - scoped_ptr m_database; simplifier m_pre_simplifier; subst_simplifier m_simplifier; basic_simplifier_plugin * m_bsimp; @@ -168,8 +167,6 @@ public: // TODO: improve precision of the following method. bool has_quantifiers() const { return m_simplifier.visited_quantifier(); /* approximation */ } - void set_pattern_database(pattern_database * db) { m_database = db; } - // ----------------------------------- // // Macros diff --git a/src/tactic/arith/fix_dl_var_tactic.cpp b/src/tactic/arith/fix_dl_var_tactic.cpp index 11feff3a0..d2e3ebf1f 100644 --- a/src/tactic/arith/fix_dl_var_tactic.cpp +++ b/src/tactic/arith/fix_dl_var_tactic.cpp @@ -329,7 +329,12 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, pc, core); + try { + (*m_imp)(in, result, mc, pc, core); + } + catch (rewriter_exception & ex) { + throw tactic_exception(ex.msg()); + } } virtual void cleanup() { diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index f9f22007a..871614c1b 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -335,7 +335,12 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, pc, core); + try { + (*m_imp)(in, result, mc, pc, core); + } + catch (rewriter_exception & ex) { + throw tactic_exception(ex.msg()); + } } virtual void cleanup() { diff --git a/src/tactic/arith/normalize_bounds_tactic.cpp b/src/tactic/arith/normalize_bounds_tactic.cpp index 5a9310ff0..f7aa968ef 100644 --- a/src/tactic/arith/normalize_bounds_tactic.cpp +++ b/src/tactic/arith/normalize_bounds_tactic.cpp @@ -181,7 +181,12 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, pc, core); + try { + (*m_imp)(in, result, mc, pc, core); + } + catch (rewriter_exception & ex) { + throw tactic_exception(ex.msg()); + } } virtual void cleanup() { diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index a68a6a000..4bea07269 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -870,22 +870,27 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - SASSERT(g->is_well_sorted()); - mc = 0; pc = 0; core = 0; - tactic_report report("purify-arith", *g); - bool produce_proofs = g->proofs_enabled(); - bool produce_models = g->models_enabled(); - bool elim_root_objs = m_params.get_bool(":elim-root-objects", true); - bool elim_inverses = m_params.get_bool(":elim-inverses", true); - bool complete = m_params.get_bool(":complete", true); - purify_arith_proc proc(m_util, m_aux_decls, produce_proofs, elim_root_objs, elim_inverses, complete); - - proc(*(g.get()), mc, produce_models); - - g->inc_depth(); - result.push_back(g.get()); - TRACE("purify_arith", g->display(tout);); - SASSERT(g->is_well_sorted()); + try { + SASSERT(g->is_well_sorted()); + mc = 0; pc = 0; core = 0; + tactic_report report("purify-arith", *g); + bool produce_proofs = g->proofs_enabled(); + bool produce_models = g->models_enabled(); + bool elim_root_objs = m_params.get_bool(":elim-root-objects", true); + bool elim_inverses = m_params.get_bool(":elim-inverses", true); + bool complete = m_params.get_bool(":complete", true); + purify_arith_proc proc(m_util, m_aux_decls, produce_proofs, elim_root_objs, elim_inverses, complete); + + proc(*(g.get()), mc, produce_models); + + g->inc_depth(); + result.push_back(g.get()); + TRACE("purify_arith", g->display(tout);); + SASSERT(g->is_well_sorted()); + } + catch (rewriter_exception & ex) { + throw tactic_exception(ex.msg()); + } } virtual void cleanup() { diff --git a/src/tactic/arith/recover_01_tactic.cpp b/src/tactic/arith/recover_01_tactic.cpp index 76f2938d8..a42bedc44 100644 --- a/src/tactic/arith/recover_01_tactic.cpp +++ b/src/tactic/arith/recover_01_tactic.cpp @@ -416,7 +416,12 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - (*m_imp)(g, result, mc, pc, core); + try { + (*m_imp)(g, result, mc, pc, core); + } + catch (rewriter_exception & ex) { + throw tactic_exception(ex.msg()); + } } virtual void cleanup() { diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 41b714172..52637b1c3 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -244,7 +244,12 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - (*m_imp)(in, result, mc, pc, core); + try { + (*m_imp)(in, result, mc, pc, core); + } + catch (rewriter_exception & ex) { + throw tactic_exception(ex.msg()); + } } virtual void cleanup() { diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp index a7ce0b39f..0408f8c8d 100644 --- a/src/tactic/core/simplify_tactic.cpp +++ b/src/tactic/core/simplify_tactic.cpp @@ -97,10 +97,15 @@ void simplify_tactic::operator()(goal_ref const & in, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - (*m_imp)(*(in.get())); - in->inc_depth(); - result.push_back(in.get()); - mc = 0; pc = 0; core = 0; + try { + (*m_imp)(*(in.get())); + in->inc_depth(); + result.push_back(in.get()); + mc = 0; pc = 0; core = 0; + } + catch (rewriter_exception & ex) { + throw tactic_exception(ex.msg()); + } } void simplify_tactic::set_cancel(bool f) { diff --git a/src/tactic/nlsat/nlsat_tactic.cpp b/src/tactic/nlsat/nlsat_tactic.cpp index 8b3c80b17..868975965 100644 --- a/src/tactic/nlsat/nlsat_tactic.cpp +++ b/src/tactic/nlsat/nlsat_tactic.cpp @@ -232,6 +232,7 @@ public: throw ex; } catch (z3_exception & ex) { + // convert all Z3 exceptions into tactic exceptions. throw tactic_exception(ex.msg()); } } diff --git a/src/tactic/subpaving/subpaving_tactic.cpp b/src/tactic/subpaving/subpaving_tactic.cpp index 17e1e72d2..7bbff4b0b 100644 --- a/src/tactic/subpaving/subpaving_tactic.cpp +++ b/src/tactic/subpaving/subpaving_tactic.cpp @@ -249,13 +249,19 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - m_imp->process(*in); - m_imp->collect_statistics(m_stats); - result.reset(); - result.push_back(in.get()); - mc = 0; - pc = 0; - core = 0; + try { + m_imp->process(*in); + m_imp->collect_statistics(m_stats); + result.reset(); + result.push_back(in.get()); + mc = 0; + pc = 0; + core = 0; + } + catch (z3_exception & ex) { + // convert all Z3 exceptions into tactic exceptions + throw tactic_exception(ex.msg()); + } } virtual void cleanup() { diff --git a/src/tactic/tactic_exception.h b/src/tactic/tactic_exception.h new file mode 100644 index 000000000..4949a2d5b --- /dev/null +++ b/src/tactic/tactic_exception.h @@ -0,0 +1,41 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + tactic_exception.h + +Abstract: + + Tactic expection object. + +Author: + + Leonardo (leonardo) 2012-08-15 + +Notes: + +--*/ +#ifndef _TACTIC_EXCEPTION_H_ +#define _TACTIC_EXCEPTION_H_ + +#include"z3_exception.h" +#include"common_msgs.h" + +class tactic_exception : public z3_exception { +protected: + std::string m_msg; +public: + tactic_exception(char const * msg):m_msg(msg) {} + virtual ~tactic_exception() {} + virtual char const * msg() const { return m_msg.c_str(); } +}; + +#define TACTIC_CANCELED_MSG Z3_CANCELED_MSG +#define TACTIC_MAX_MEMORY_MSG Z3_MAX_MEMORY_MSG +#define TACTIC_MAX_SCOPES_MSG Z3_MAX_SCOPES_MSG +#define TACTIC_MAX_STEPS_MSG Z3_MAX_STEPS_MSG +#define TACTIC_MAX_FRAMES_MSG Z3_MAX_FRAMES_MSG +#define TACTIC_NO_PROOF_GEN_MSG Z3_NO_PROOF_GEN_MSG + +#endif diff --git a/src/util/common_msgs.cpp b/src/util/common_msgs.cpp new file mode 100644 index 000000000..630a9f4c6 --- /dev/null +++ b/src/util/common_msgs.cpp @@ -0,0 +1,26 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + common_msgs.cpp + +Abstract: + + Common messages used in Z3. + +Author: + + Leonardo (leonardo) 2012-10-25 + +Notes: + +--*/ +#include"common_msgs.h" + +char const * common_msgs::g_canceled_msg = "canceled"; +char const * common_msgs::g_max_memory_msg = "max. memory exceeded"; +char const * common_msgs::g_max_scopes_msg = "max. scopes exceeded"; +char const * common_msgs::g_max_steps_msg = "max. steps exceeded"; +char const * common_msgs::g_max_frames_msg = "max. frames exceeded"; +char const * common_msgs::g_no_proofs_msg = "component does not support proof generation"; diff --git a/src/util/common_msgs.h b/src/util/common_msgs.h new file mode 100644 index 000000000..1ffdbf06c --- /dev/null +++ b/src/util/common_msgs.h @@ -0,0 +1,39 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + common_msgs.h + +Abstract: + + Common messages used in Z3. + +Author: + + Leonardo (leonardo) 2012-10-25 + +Notes: + +--*/ +#ifndef __COMMON_MSGS_H_ +#define __COMMON_MSGS_H_ + +class common_msgs { +public: + static char const * g_canceled_msg; + static char const * g_max_memory_msg; + static char const * g_max_scopes_msg; + static char const * g_max_steps_msg; + static char const * g_max_frames_msg; + static char const * g_no_proofs_msg; +}; + +#define Z3_CANCELED_MSG common_msgs::g_canceled_msg +#define Z3_MAX_MEMORY_MSG common_msgs::g_max_memory_msg +#define Z3_MAX_SCOPES_MSG common_msgs::g_max_scopes_msg +#define Z3_MAX_STEPS_MSG common_msgs::g_max_steps_msg +#define Z3_MAX_FRAMES_MSG common_msgs::g_max_frames_msg +#define Z3_NO_PROOF_GEN_MSG common_msgs::g_no_proofs_msg + +#endif diff --git a/src/util/tactic_exception.cpp b/src/util/tactic_exception.cpp deleted file mode 100644 index 73cd37162..000000000 --- a/src/util/tactic_exception.cpp +++ /dev/null @@ -1,26 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - tactic_exception.cpp - -Abstract: - - Tactic expection object. - -Author: - - Leonardo (leonardo) 2012-08-15 - -Notes: - ---*/ -#include"tactic_exception.h" - -char const * tactic_exception::g_tactic_canceled_msg = "canceled"; -char const * tactic_exception::g_tactic_max_memory_msg = "max. memory exceeded"; -char const * tactic_exception::g_tactic_max_scopes_msg = "max. scopes exceeded"; -char const * tactic_exception::g_tactic_max_steps_msg = "max. steps exceeded"; -char const * tactic_exception::g_tactic_max_frames_msg = "max. frames exceeded"; -char const * tactic_exception::g_tactic_no_proofs_msg = "tactic does not support proof generation"; diff --git a/src/util/tactic_exception.h b/src/util/tactic_exception.h deleted file mode 100644 index 16272260e..000000000 --- a/src/util/tactic_exception.h +++ /dev/null @@ -1,47 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - tactic_exception.h - -Abstract: - - Tactic expection object. - -Author: - - Leonardo (leonardo) 2012-08-15 - -Notes: - ---*/ -#ifndef _TACTIC_EXCEPTION_H_ -#define _TACTIC_EXCEPTION_H_ - -#include"z3_exception.h" - -class tactic_exception : public z3_exception { -public: - static char const * g_tactic_canceled_msg; - static char const * g_tactic_max_memory_msg; - static char const * g_tactic_max_scopes_msg; - static char const * g_tactic_max_steps_msg; - static char const * g_tactic_max_frames_msg; - static char const * g_tactic_no_proofs_msg; -protected: - std::string m_msg; -public: - tactic_exception(char const * msg):m_msg(msg) {} - virtual ~tactic_exception() {} - virtual char const * msg() const { return m_msg.c_str(); } -}; - -#define TACTIC_CANCELED_MSG tactic_exception::g_tactic_canceled_msg -#define TACTIC_MAX_MEMORY_MSG tactic_exception::g_tactic_max_memory_msg -#define TACTIC_MAX_SCOPES_MSG tactic_exception::g_tactic_max_scopes_msg -#define TACTIC_MAX_STEPS_MSG tactic_exception::g_tactic_max_steps_msg -#define TACTIC_MAX_FRAMES_MSG tactic_exception::g_tactic_max_frames_msg -#define TACTIC_NO_PROOF_GEN_MSG tactic_exception::g_tactic_no_proofs_msg - -#endif