From 45af1bd243d0561f4abd808e16cc4b74e44daa2e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 14 Feb 2021 14:40:29 -0800
Subject: [PATCH] fix build, move seq_skolem
---
src/ast/rewriter/CMakeLists.txt | 1 +
src/{smt => ast/rewriter}/seq_skolem.cpp | 2 +-
src/{smt => ast/rewriter}/seq_skolem.h | 0
src/sat/smt/recfun_solver.cpp | 4 ++--
src/sat/smt/recfun_solver.h | 10 +++++-----
src/smt/CMakeLists.txt | 1 -
src/smt/seq_axioms.h | 2 +-
src/smt/seq_regex.h | 2 +-
src/smt/theory_seq.h | 2 +-
9 files changed, 12 insertions(+), 12 deletions(-)
rename src/{smt => ast/rewriter}/seq_skolem.cpp (99%)
rename src/{smt => ast/rewriter}/seq_skolem.h (100%)
diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt
index c57b02b98..105bd86af 100644
--- a/src/ast/rewriter/CMakeLists.txt
+++ b/src/ast/rewriter/CMakeLists.txt
@@ -33,6 +33,7 @@ z3_add_component(rewriter
recfun_rewriter.cpp
rewriter.cpp
seq_rewriter.cpp
+ seq_skolem.cpp
th_rewriter.cpp
value_sweep.cpp
var_subst.cpp
diff --git a/src/smt/seq_skolem.cpp b/src/ast/rewriter/seq_skolem.cpp
similarity index 99%
rename from src/smt/seq_skolem.cpp
rename to src/ast/rewriter/seq_skolem.cpp
index d4f16f783..33f192ceb 100644
--- a/src/smt/seq_skolem.cpp
+++ b/src/ast/rewriter/seq_skolem.cpp
@@ -11,7 +11,7 @@ Author:
--*/
-#include "smt/seq_skolem.h"
+#include "ast/rewriter/seq_skolem.h"
#include "ast/ast_pp.h"
using namespace smt;
diff --git a/src/smt/seq_skolem.h b/src/ast/rewriter/seq_skolem.h
similarity index 100%
rename from src/smt/seq_skolem.h
rename to src/ast/rewriter/seq_skolem.h
diff --git a/src/sat/smt/recfun_solver.cpp b/src/sat/smt/recfun_solver.cpp
index 0da80ebdd..40d5299c4 100644
--- a/src/sat/smt/recfun_solver.cpp
+++ b/src/sat/smt/recfun_solver.cpp
@@ -149,7 +149,7 @@ namespace recfun {
m_guard2pending.insert(guard, alloc(expr_ref_vector, guards));
}
TRACEFN("add clause\n" << core);
- push_core(core);
+ push_c(core);
}
/**
@@ -228,7 +228,7 @@ namespace recfun {
return true;
}
- void solver::push(propagation_item* p) {
+ void solver::push_prop(propagation_item* p) {
m_propagation_queue.push_back(p);
ctx.push(push_back_vector<scoped_ptr_vector<propagation_item>>(m_propagation_queue));
}
diff --git a/src/sat/smt/recfun_solver.h b/src/sat/smt/recfun_solver.h
index f8ce8f2e6..cfdf6fe63 100644
--- a/src/sat/smt/recfun_solver.h
+++ b/src/sat/smt/recfun_solver.h
@@ -52,11 +52,11 @@ namespace recfun {
scoped_ptr_vector<propagation_item> m_propagation_queue;
unsigned m_qhead { 0 };
- void push_body_expand(expr* e) { push(alloc(propagation_item, alloc(body_expansion, u(), to_app(e)))); }
- void push_case_expand(expr* e) { push(alloc(propagation_item, alloc(case_expansion, u(), to_app(e)))); }
- void push_guard(expr* e) { push(alloc(propagation_item, e)); }
- void push_core(expr_ref_vector const& core) { push(alloc(propagation_item, core)); }
- void push(propagation_item* p);
+ void push_body_expand(expr* e) { push_prop(alloc(propagation_item, alloc(body_expansion, u(), to_app(e)))); }
+ void push_case_expand(expr* e) { push_prop(alloc(propagation_item, alloc(case_expansion, u(), to_app(e)))); }
+ void push_guard(expr* e) { push_prop(alloc(propagation_item, e)); }
+ void push_c(expr_ref_vector const& core) { push_prop(alloc(propagation_item, core)); }
+ void push_prop(propagation_item* p);
bool is_enabled_guard(expr* guard) { return m_enabled_guards.contains(guard); }
bool is_disabled_guard(expr* guard) { return m_disabled_guards.contains(guard); }
diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
index 78cae3321..427c2c9cf 100644
--- a/src/smt/CMakeLists.txt
+++ b/src/smt/CMakeLists.txt
@@ -14,7 +14,6 @@ z3_add_component(smt
seq_ne_solver.cpp
seq_offset_eq.cpp
seq_regex.cpp
- seq_skolem.cpp
smt_almost_cg_table.cpp
smt_arith_value.cpp
smt_case_split_queue.cpp
diff --git a/src/smt/seq_axioms.h b/src/smt/seq_axioms.h
index 65f883564..4f27f8ab5 100644
--- a/src/smt/seq_axioms.h
+++ b/src/smt/seq_axioms.h
@@ -22,8 +22,8 @@ Revision History:
#include "ast/seq_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
#include "ast/rewriter/th_rewriter.h"
+#include "ast/rewriter/seq_skolem.h"
#include "smt/smt_theory.h"
-#include "smt/seq_skolem.h"
namespace smt {
diff --git a/src/smt/seq_regex.h b/src/smt/seq_regex.h
index acd316cb5..983032979 100644
--- a/src/smt/seq_regex.h
+++ b/src/smt/seq_regex.h
@@ -20,8 +20,8 @@ Author:
#include "util/state_graph.h"
#include "ast/seq_decl_plugin.h"
#include "ast/rewriter/seq_rewriter.h"
+#include "ast/rewriter/seq_skolem.h"
#include "smt/smt_context.h"
-#include "smt/seq_skolem.h"
/*
*** Tracing and debugging in this module and related modules ***
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index d9f73e541..011cebe1a 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -29,7 +29,7 @@ Revision History:
#include "smt/smt_theory.h"
#include "smt/smt_arith_value.h"
#include "smt/theory_seq_empty.h"
-#include "smt/seq_skolem.h"
+#include "ast/rewriter/seq_skolem.h"
#include "smt/seq_axioms.h"
#include "smt/seq_regex.h"
#include "smt/seq_offset_eq.h"