mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-08 04:01:22 +00:00
Code Activity

rename pdr_tactic to horn_tactic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-19 09:24:19 -08:00
parent b30fc79bf1
commit 62c713129a
3 changed files with 18 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/muz_qe/pdr_tactic.cpp → src/muz_qe/horn_tactic.cpp
View file

@ -3,11 +3,11 @@ Copyright (c) 2012 Microsoft Corporation
Module Name: Module Name:
pdr_tactic.h horn_tactic.h
Abstract: Abstract:
PDR as a tactic to solve Horn clauses. HORN as a tactic to solve Horn clauses.
Author: Author:
@ -19,10 +19,10 @@ Revision History:
#include"tactical.h" #include"tactical.h"
#include"model_converter.h" #include"model_converter.h"
#include"proof_converter.h" #include"proof_converter.h"
#include"pdr_tactic.h" #include"horn_tactic.h"
#include"dl_context.h" #include"dl_context.h"
class pdr_tactic : public tactic { class horn_tactic : public tactic {
struct imp { struct imp {
ast_manager& m; ast_manager& m;
datalog::context m_ctx; datalog::context m_ctx;
@ -139,7 +139,7 @@ class pdr_tactic : public tactic {
expr_dependency_ref & core) { expr_dependency_ref & core) {
SASSERT(g->is_well_sorted()); SASSERT(g->is_well_sorted());
mc = 0; pc = 0; core = 0; mc = 0; pc = 0; core = 0;
tactic_report report("pdr", *g); tactic_report report("horn", *g);
bool produce_models = g->models_enabled(); bool produce_models = g->models_enabled();
bool produce_proofs = g->proofs_enabled(); bool produce_proofs = g->proofs_enabled();
@ -210,7 +210,7 @@ class pdr_tactic : public tactic {
// subgoal is unchanged. // subgoal is unchanged.
break; break;
} }
TRACE("pdr", g->display(tout);); TRACE("horn", g->display(tout););
SASSERT(g->is_well_sorted()); SASSERT(g->is_well_sorted());
} }
}; };
@ -218,16 +218,16 @@ class pdr_tactic : public tactic {
params_ref m_params; params_ref m_params;
imp * m_imp; imp * m_imp;
public: public:
pdr_tactic(ast_manager & m, params_ref const & p): horn_tactic(ast_manager & m, params_ref const & p):
m_params(p) { m_params(p) {
m_imp = alloc(imp, m, p); m_imp = alloc(imp, m, p);
} }
virtual tactic * translate(ast_manager & m) { virtual tactic * translate(ast_manager & m) {
return alloc(pdr_tactic, m, m_params); return alloc(horn_tactic, m, m_params);
} }
virtual ~pdr_tactic() { virtual ~horn_tactic() {
dealloc(m_imp); dealloc(m_imp);
} }
@ -281,7 +281,7 @@ protected:
} }
}; };
tactic * mk_pdr_tactic(ast_manager & m, params_ref const & p) { tactic * mk_horn_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(pdr_tactic, m, p)); return clean(alloc(horn_tactic, m, p));
} }

10
src/muz_qe/pdr_tactic.h → src/muz_qe/horn_tactic.h
View file

@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation
Module Name: Module Name:
pdr_tactic.h horn_tactic.h
Abstract: Abstract:
@ -16,15 +16,15 @@ Author:
Revision History: Revision History:
--*/ --*/
#ifndef _PDR_TACTIC_H_ #ifndef _HORN_TACTIC_H_
#define _PDR_TACTIC_H_ #define _HORN_TACTIC_H_
#include"params.h" #include"params.h"
class ast_manager; class ast_manager;
class tactic; class tactic;
tactic * mk_pdr_tactic(ast_manager & m, params_ref const & p = params_ref()); tactic * mk_horn_tactic(ast_manager & m, params_ref const & p = params_ref());
/* /*
ADD_TACTIC("pdr", "apply pdr for horn clauses.", "mk_pdr_tactic(m, p)") ADD_TACTIC("horn", "apply tactic for horn clauses.", "mk_horn_tactic(m, p)")
*/ */
#endif #endif

4
src/tactic/portfolio/smt_strategic_solver.cpp
View file

@ -33,7 +33,7 @@ Notes:
#include"default_tactic.h" #include"default_tactic.h"
#include"ufbv_tactic.h" #include"ufbv_tactic.h"
#include"qffpa_tactic.h" #include"qffpa_tactic.h"
#include"pdr_tactic.h" #include"horn_tactic.h"
#include"smt_solver.h" #include"smt_solver.h"
MK_SIMPLE_TACTIC_FACTORY(qfuf_fct, mk_qfuf_tactic(m, p)); MK_SIMPLE_TACTIC_FACTORY(qfuf_fct, mk_qfuf_tactic(m, p));
@ -55,7 +55,7 @@ MK_SIMPLE_TACTIC_FACTORY(qfnia_fct, mk_qfnia_tactic(m, p));
MK_SIMPLE_TACTIC_FACTORY(qfnra_fct, mk_qfnra_tactic(m, p)); MK_SIMPLE_TACTIC_FACTORY(qfnra_fct, mk_qfnra_tactic(m, p));
MK_SIMPLE_TACTIC_FACTORY(qffpa_fct, mk_qffpa_tactic(m, p)); MK_SIMPLE_TACTIC_FACTORY(qffpa_fct, mk_qffpa_tactic(m, p));
MK_SIMPLE_TACTIC_FACTORY(ufbv_fct, mk_ufbv_tactic(m, p)); MK_SIMPLE_TACTIC_FACTORY(ufbv_fct, mk_ufbv_tactic(m, p));
MK_SIMPLE_TACTIC_FACTORY(horn_fct, mk_pdr_tactic(m, p)); MK_SIMPLE_TACTIC_FACTORY(horn_fct, mk_horn_tactic(m, p));
static void init(strategic_solver * s) { static void init(strategic_solver * s) {
s->set_default_tactic(alloc(default_fct)); s->set_default_tactic(alloc(default_fct));