From 10cd396ae3ad8439448175f9957e2e962aa6e04c Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 31 Aug 2017 17:21:44 -0400 Subject: [PATCH 1/9] rewriter patch for theory_str --- src/smt/theory_str.cpp | 84 +++++++++++++++++++----------------------- 1 file changed, 37 insertions(+), 47 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 89e0123a8..0ddf24596 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -14,17 +14,17 @@ Revision History: --*/ -#include"ast_smt2_pp.h" -#include"smt_context.h" -#include"theory_str.h" -#include"smt_model_generator.h" -#include"ast_pp.h" -#include"ast_ll_pp.h" +#include "ast/ast_smt2_pp.h" +#include "smt/smt_context.h" +#include "smt/theory_str.h" +#include "smt/smt_model_generator.h" +#include "ast/ast_pp.h" +#include "ast/ast_ll_pp.h" #include #include -#include"theory_seq_empty.h" -#include"theory_arith.h" -#include"ast_util.h" +#include "smt/theory_seq_empty.h" +#include "smt/theory_arith.h" +#include "ast/ast_util.h" namespace smt { @@ -166,14 +166,18 @@ namespace smt { } } - void theory_str::assert_axiom(expr * e) { + void theory_str::assert_axiom(expr * _e) { if (opt_VerifyFinalCheckProgress) { finalCheckProgressIndicator = true; } - if (get_manager().is_true(e)) return; - TRACE("str", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;); + if (get_manager().is_true(_e)) return; context & ctx = get_context(); + ast_manager& m = get_manager(); + TRACE("str", tout << "asserting " << mk_ismt2_pp(_e, m) << std::endl;); + expr_ref e(_e, m); + th_rewriter rw(m); + rw(e); if (!ctx.b_internalized(e)) { ctx.internalize(e, false); } @@ -1419,6 +1423,9 @@ namespace smt { void theory_str::instantiate_axiom_Substr(enode * e) { context & ctx = get_context(); ast_manager & m = get_manager(); + expr* substrBase = 0; + expr* substrPos = 0; + expr* substrLen = 0; app * expr = e->get_owner(); if (axiomatized_terms.contains(expr)) { @@ -1429,12 +1436,7 @@ namespace smt { TRACE("str", tout << "instantiate Substr axiom for " << mk_pp(expr, m) << std::endl;); - expr_ref substrBase(expr->get_arg(0), m); - expr_ref substrPos(expr->get_arg(1), m); - expr_ref substrLen(expr->get_arg(2), m); - SASSERT(substrBase); - SASSERT(substrPos); - SASSERT(substrLen); + VERIFY(u.str.is_extract(expr, substrBase, substrPos, substrLen)); expr_ref zero(m_autil.mk_numeral(rational::zero(), true), m); expr_ref minusOne(m_autil.mk_numeral(rational::minus_one(), true), m); @@ -1452,28 +1454,19 @@ namespace smt { // len >= 0 argumentsValid_terms.push_back(m_autil.mk_ge(substrLen, zero)); - expr_ref argumentsValid(mk_and(argumentsValid_terms), m); - SASSERT(argumentsValid); - ctx.internalize(argumentsValid, false); // (pos+len) >= strlen(base) // --> pos + len + -1*strlen(base) >= 0 expr_ref lenOutOfBounds(m_autil.mk_ge( m_autil.mk_add(substrPos, substrLen, m_autil.mk_mul(minusOne, mk_strlen(substrBase))), zero), m); - SASSERT(lenOutOfBounds); - ctx.internalize(argumentsValid, false); + expr_ref argumentsValid = mk_and(argumentsValid_terms); // Case 1: pos < 0 or pos >= strlen(base) or len < 0 // ==> (Substr ...) = "" expr_ref case1_premise(m.mk_not(argumentsValid), m); - SASSERT(case1_premise); - ctx.internalize(case1_premise, false); expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m); - SASSERT(case1_conclusion); - ctx.internalize(case1_conclusion, false); - expr_ref case1(rewrite_implication(case1_premise, case1_conclusion), m); - SASSERT(case1); + expr_ref case1(m.mk_implies(case1_premise, case1_conclusion), m); // Case 2: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) >= strlen(base) // ==> base = t0.t1 AND len(t0) = pos AND (Substr ...) = t1 @@ -1483,8 +1476,7 @@ namespace smt { ctx.mk_eq_atom(substrBase, mk_concat(t0,t1)), ctx.mk_eq_atom(mk_strlen(t0), substrPos), ctx.mk_eq_atom(expr, t1)), m); - expr_ref case2(rewrite_implication(m.mk_and(argumentsValid, lenOutOfBounds), case2_conclusion), m); - SASSERT(case2); + expr_ref case2(m.mk_implies(m.mk_and(argumentsValid, lenOutOfBounds), case2_conclusion), m); // Case 3: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) < strlen(base) // ==> base = t2.t3.t4 AND len(t2) = pos AND len(t3) = len AND (Substr ...) = t3 @@ -1497,16 +1489,11 @@ namespace smt { case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen)); case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3)); expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m); - expr_ref case3(rewrite_implication(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m); - SASSERT(case3); + expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m); - ctx.internalize(case1, false); - ctx.internalize(case2, false); - ctx.internalize(case3, false); - - expr_ref finalAxiom(m.mk_and(case1, case2, case3), m); - SASSERT(finalAxiom); - assert_axiom(finalAxiom); + assert_axiom(case1); + assert_axiom(case2); + assert_axiom(case3); } void theory_str::instantiate_axiom_Replace(enode * e) { @@ -1549,14 +1536,12 @@ namespace smt { expr_ref elseBranch(ctx.mk_eq_atom(result, expr->get_arg(0)), m); expr_ref breakdownAssert(m.mk_ite(condAst, m.mk_and(thenItems.size(), thenItems.c_ptr()), elseBranch), m); + assert_axiom(breakdownAssert); + SASSERT(breakdownAssert); expr_ref reduceToResult(ctx.mk_eq_atom(expr, result), m); - SASSERT(reduceToResult); - - expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToResult), m); - SASSERT(finalAxiom); - assert_axiom(finalAxiom); + assert_axiom(reduceToResult); } void theory_str::instantiate_axiom_str_to_int(enode * e) { @@ -4658,7 +4643,7 @@ namespace smt { // safety if (!ctx.e_internalized(e)) { - return false; + return false; } // if an integer constant exists in the eqc, it should be the root @@ -8422,6 +8407,7 @@ namespace smt { // Check agreement between integer and string theories for the term a = (str.to-int S). // Returns true if axioms were added, and false otherwise. bool theory_str::finalcheck_str2int(app * a) { + SASSERT(u.str.is_stoi(a)); bool axiomAdd = false; context & ctx = get_context(); ast_manager & m = get_manager(); @@ -8448,7 +8434,11 @@ namespace smt { } } else { TRACE("str", tout << "integer theory has no assignment for " << mk_pp(a, m) << std::endl;); - NOT_IMPLEMENTED_YET(); + expr_ref is_zero(ctx.mk_eq_atom(a, m_autil.mk_int(0)), m); + literal is_zero_l = mk_literal(is_zero); + axiomAdd = true; + TRACE("str", ctx.display(tout);); + // NOT_IMPLEMENTED_YET(); } return axiomAdd; From 4e4c72580b29d57d376fb425d49f9f397a539cd3 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 7 Sep 2017 14:06:37 -0400 Subject: [PATCH 2/9] don't rewrite on every axiom in theory_str --- src/smt/theory_str.cpp | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 0ddf24596..f59c06fae 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -176,8 +176,8 @@ namespace smt { ast_manager& m = get_manager(); TRACE("str", tout << "asserting " << mk_ismt2_pp(_e, m) << std::endl;); expr_ref e(_e, m); - th_rewriter rw(m); - rw(e); + //th_rewriter rw(m); + //rw(e); if (!ctx.b_internalized(e)) { ctx.internalize(e, false); } @@ -1491,9 +1491,21 @@ namespace smt { expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m); expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m); - assert_axiom(case1); - assert_axiom(case2); - assert_axiom(case3); + { + th_rewriter rw(m); + + expr_ref case1_rw(case1, m); + rw(case1_rw); + assert_axiom(case1_rw); + + expr_ref case2_rw(case2, m); + rw(case2_rw); + assert_axiom(case2_rw); + + expr_ref case3_rw(case3, m); + rw(case3_rw); + assert_axiom(case3_rw); + } } void theory_str::instantiate_axiom_Replace(enode * e) { From 1ce68b3794d9bac95383d3f915bf0f2819ee22de Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 7 Sep 2017 14:53:34 -0400 Subject: [PATCH 3/9] rewrite theory_str replace instances --- src/smt/theory_str.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index f59c06fae..0322b736d 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1547,13 +1547,17 @@ namespace smt { // false branch expr_ref elseBranch(ctx.mk_eq_atom(result, expr->get_arg(0)), m); + th_rewriter rw(m); + expr_ref breakdownAssert(m.mk_ite(condAst, m.mk_and(thenItems.size(), thenItems.c_ptr()), elseBranch), m); - assert_axiom(breakdownAssert); - - SASSERT(breakdownAssert); + expr_ref breakdownAssert_rw(breakdownAssert, m); + rw(breakdownAssert_rw); + assert_axiom(breakdownAssert_rw); expr_ref reduceToResult(ctx.mk_eq_atom(expr, result), m); - assert_axiom(reduceToResult); + expr_ref reduceToResult_rw(reduceToResult, m); + rw(reduceToResult_rw); + assert_axiom(reduceToResult_rw); } void theory_str::instantiate_axiom_str_to_int(enode * e) { From b2af690c6d38bbbaeaae4e0311eb69ab48fa79cb Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 22 Sep 2017 12:31:46 -0400 Subject: [PATCH 4/9] enable binary search for theory_str --- src/smt/params/smt_params_helper.pyg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index d6ca8c9b2..937aa6a2b 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -74,7 +74,7 @@ def_module_params(module_name='smt', ('str.fast_length_tester_cache', BOOL, False, 'cache length tester constants instead of regenerating them'), ('str.fast_value_tester_cache', BOOL, True, 'cache value tester constants instead of regenerating them'), ('str.string_constant_cache', BOOL, True, 'cache all generated string constants generated from anywhere in theory_str'), - ('str.use_binary_search', BOOL, False, 'use a binary search heuristic for finding concrete length values for free variables in theory_str (set to False to use linear search)'), + ('str.use_binary_search', BOOL, True, 'use a binary search heuristic for finding concrete length values for free variables in theory_str (set to False to use linear search)'), ('str.binary_search_start', UINT, 64, 'initial upper bound for theory_str binary search'), ('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'), ('str.finite_overlap_models', BOOL, False, 'attempt a finite model search for overlapping variables instead of completely giving up on the arrangement'), From 317e2b189848f65cd7d55d08acbf65f2111b5824 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 22 Sep 2017 12:32:13 -0400 Subject: [PATCH 5/9] take shortcuts during length testing when length is known from integer theory --- src/smt/theory_str.cpp | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 8a141665c..fe00bb35d 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -10229,9 +10229,30 @@ namespace smt { expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, zstring lenTesterValue) { ast_manager & m = get_manager(); + context & ctx = get_context(); TRACE("str", tout << "gen for free var " << mk_ismt2_pp(freeVar, m) << std::endl;); + // special case: if we would be length testing for the first time, + // but already know a value for length from the integer solver, + // don't give any other options + { + rational freeVar_len; + if (lenTesterInCbEq == NULL && get_len_value(freeVar, freeVar_len)) { + TRACE("str", tout << "length of free var " << mk_pp(freeVar, m) << " already given to be " << freeVar_len << std::endl;); + expr * newTester = mk_internal_lenTest_var(freeVar, 0); + expr * concreteLength_lhs = ctx.mk_eq_atom(newTester, mk_string(freeVar_len.to_string().c_str())); + expr * concreteLength_rhs = ctx.mk_eq_atom(mk_strlen(freeVar), m_autil.mk_numeral(freeVar_len, true)); + expr * concreteLength_assert = ctx.mk_eq_atom(concreteLength_lhs, concreteLength_rhs); + m_trail.push_back(concreteLength_assert); + TRACE("str", tout << mk_pp(concreteLength_assert, m) << std::endl;); + expr * valueAssert = gen_free_var_options(freeVar, newTester, zstring(freeVar_len.to_string().c_str()), NULL, zstring("")); + m_trail.push_back(valueAssert); + TRACE("str", tout << mk_pp(valueAssert, m) << std::endl;); + return m.mk_and(concreteLength_assert, valueAssert); + } + } + if (m_params.m_UseBinarySearch) { TRACE("str", tout << "using binary search heuristic" << std::endl;); return binary_search_length_test(freeVar, lenTesterInCbEq, lenTesterValue); From ec7ea8a763f6b5647ab53db289131082b69f61b4 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 25 Sep 2017 15:21:59 -0400 Subject: [PATCH 6/9] redo length testing with concrete length, linear search only --- src/smt/theory_str.cpp | 35 +++++++++++++++-------------------- 1 file changed, 15 insertions(+), 20 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index fe00bb35d..70e564a50 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -9887,6 +9887,21 @@ namespace smt { expr_ref freeVarLen(mk_strlen(freeVar), m); SASSERT(freeVarLen); + { + rational freeVar_len_value; + if (get_len_value(freeVar, freeVar_len_value)) { + TRACE("str", tout << "special case: length of freeVar is known to be " << freeVar_len_value << std::endl;); + expr_ref concreteOption(ctx.mk_eq_atom(indicator, mk_string(freeVar_len_value.to_string().c_str()) ), m); + expr_ref concreteValue(ctx.mk_eq_atom( + ctx.mk_eq_atom(indicator, mk_string(freeVar_len_value.to_string().c_str()) ), + ctx.mk_eq_atom(freeVarLen, m_autil.mk_numeral(freeVar_len_value, true))), m); + expr_ref finalAxiom(m.mk_and(concreteOption, concreteValue), m); + SASSERT(finalAxiom); + m_trail.push_back(finalAxiom); + return finalAxiom; + } + } + expr_ref_vector orList(m); expr_ref_vector andList(m); @@ -10233,26 +10248,6 @@ namespace smt { TRACE("str", tout << "gen for free var " << mk_ismt2_pp(freeVar, m) << std::endl;); - // special case: if we would be length testing for the first time, - // but already know a value for length from the integer solver, - // don't give any other options - { - rational freeVar_len; - if (lenTesterInCbEq == NULL && get_len_value(freeVar, freeVar_len)) { - TRACE("str", tout << "length of free var " << mk_pp(freeVar, m) << " already given to be " << freeVar_len << std::endl;); - expr * newTester = mk_internal_lenTest_var(freeVar, 0); - expr * concreteLength_lhs = ctx.mk_eq_atom(newTester, mk_string(freeVar_len.to_string().c_str())); - expr * concreteLength_rhs = ctx.mk_eq_atom(mk_strlen(freeVar), m_autil.mk_numeral(freeVar_len, true)); - expr * concreteLength_assert = ctx.mk_eq_atom(concreteLength_lhs, concreteLength_rhs); - m_trail.push_back(concreteLength_assert); - TRACE("str", tout << mk_pp(concreteLength_assert, m) << std::endl;); - expr * valueAssert = gen_free_var_options(freeVar, newTester, zstring(freeVar_len.to_string().c_str()), NULL, zstring("")); - m_trail.push_back(valueAssert); - TRACE("str", tout << mk_pp(valueAssert, m) << std::endl;); - return m.mk_and(concreteLength_assert, valueAssert); - } - } - if (m_params.m_UseBinarySearch) { TRACE("str", tout << "using binary search heuristic" << std::endl;); return binary_search_length_test(freeVar, lenTesterInCbEq, lenTesterValue); From 7b536e910ee0dba7088f47f5f69fd3392998c8a6 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 13 Oct 2017 11:39:33 -0400 Subject: [PATCH 7/9] take shortcuts during binary search length testing when length is known from integer theory --- src/smt/theory_str.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 70e564a50..644863919 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -10216,6 +10216,16 @@ namespace smt { } refresh_theory_var(firstTester); + { + rational freeVar_len_value; + if (get_len_value(freeVar, freeVar_len_value)) { + TRACE("str", tout << "special case: length of freeVar is known to be " << freeVar_len_value << std::endl;); + midPoint = freeVar_len_value; + upperBound = midPoint * 2; + windowSize = upperBound; + } + } + binary_search_len_tester_stack[freeVar].push_back(firstTester); m_trail_stack.push(binary_search_trail(binary_search_len_tester_stack, freeVar)); binary_search_info new_info(lowerBound, midPoint, upperBound, windowSize); @@ -10244,7 +10254,6 @@ namespace smt { expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, zstring lenTesterValue) { ast_manager & m = get_manager(); - context & ctx = get_context(); TRACE("str", tout << "gen for free var " << mk_ismt2_pp(freeVar, m) << std::endl;); From e50470f2c4d561e42989d74b1a49e606c8e84415 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 30 Oct 2017 18:24:38 +0000 Subject: [PATCH 8/9] Added support for MSYS2 --- scripts/mk_util.py | 25 +++++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 6f3052f6e..8d4fe5552 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -72,6 +72,7 @@ IS_FREEBSD=False IS_OPENBSD=False IS_CYGWIN=False IS_CYGWIN_MINGW=False +IS_MSYS2=False VERBOSE=True DEBUG_MODE=False SHOW_CPPS = True @@ -152,6 +153,9 @@ def is_cygwin(): def is_cygwin_mingw(): return IS_CYGWIN_MINGW +def is_msys2(): + return IS_MSYS2 + def norm_path(p): return os.path.expanduser(os.path.normpath(p)) @@ -227,7 +231,7 @@ def rmf(fname): def exec_compiler_cmd(cmd): r = exec_cmd(cmd) - if is_windows() or is_cygwin_mingw(): + if is_windows() or is_cygwin_mingw() or is_cygwin() or is_msys2(): rmf('a.exe') else: rmf('a.out') @@ -606,6 +610,13 @@ elif os.name == 'posix': IS_CYGWIN=True if (CC != None and "mingw" in CC): IS_CYGWIN_MINGW=True + elif os.uname()[0].startswith('MSYS_NT'): + IS_MSYS2=True + if os.uname()[4] == 'x86_64': + LINUX_X64=True + else: + LINUX_X64=False + def display_help(exit_code): print("mk_make.py: Z3 Makefile generator\n") @@ -1229,7 +1240,7 @@ def get_so_ext(): sysname = os.uname()[0] if sysname == 'Darwin': return 'dylib' - elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD': + elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD' or sysname.startswith('MSYS_NT'): return 'so' elif sysname == 'CYGWIN': return 'dll' @@ -1783,6 +1794,8 @@ class JavaDLLComponent(Component): t = t.replace('PLATFORM', 'openbsd') elif IS_CYGWIN: t = t.replace('PLATFORM', 'cygwin') + elif IS_MSYS2: + t = t.replace('PLATFORM', 'win32') else: t = t.replace('PLATFORM', 'win32') out.write(t) @@ -2446,7 +2459,7 @@ def mk_config(): if sysname == 'Darwin': SO_EXT = '.dylib' SLIBFLAGS = '-dynamiclib' - elif sysname == 'Linux': + elif sysname == 'Linux' or sysname.startswith('MSYS_NT'): CXXFLAGS = '%s -D_LINUX_' % CXXFLAGS OS_DEFINES = '-D_LINUX_' SO_EXT = '.so' @@ -2466,10 +2479,10 @@ def mk_config(): SO_EXT = '.so' SLIBFLAGS = '-shared' elif sysname[:6] == 'CYGWIN': - CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS + CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS OS_DEFINES = '-D_CYGWIN' - SO_EXT = '.dll' - SLIBFLAGS = '-shared' + SO_EXT = '.dll' + SLIBFLAGS = '-shared' else: raise MKException('Unsupported platform: %s' % sysname) if is64(): From 34f24aee720721b844fb566d852ef88934c31e00 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 30 Oct 2017 13:50:31 -0500 Subject: [PATCH 9/9] fix order of instantiation for recursive functions, #1274 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index c508a65cb..7b508c7d8 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4389,7 +4389,8 @@ namespace smt { subst.push_back(arg); } expr_ref bodyr(m); - var_subst sub(m, false); + var_subst sub(m, true); + TRACE("context", tout << expr_ref(q, m) << " " << subst << "\n";); sub(body, subst.size(), subst.c_ptr(), bodyr); func_decl* f = to_app(fn)->get_decl(); func_interp* fi = alloc(func_interp, m, f->get_arity());