From 62c713129aa37731b4afef4df04ad33dd36b3093 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 19 Nov 2012 09:24:19 -0800
Subject: [PATCH] rename pdr_tactic to horn_tactic

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 .../{pdr_tactic.cpp => horn_tactic.cpp}       | 22 +++++++++----------
 src/muz_qe/{pdr_tactic.h => horn_tactic.h}    | 10 ++++-----
 src/tactic/portfolio/smt_strategic_solver.cpp |  4 ++--
 3 files changed, 18 insertions(+), 18 deletions(-)
 rename src/muz_qe/{pdr_tactic.cpp => horn_tactic.cpp} (94%)
 rename src/muz_qe/{pdr_tactic.h => horn_tactic.h} (53%)

diff --git a/src/muz_qe/pdr_tactic.cpp b/src/muz_qe/horn_tactic.cpp
similarity index 94%
rename from src/muz_qe/pdr_tactic.cpp
rename to src/muz_qe/horn_tactic.cpp
index 6bf9e8ed1..1e76faf13 100644
--- a/src/muz_qe/pdr_tactic.cpp
+++ b/src/muz_qe/horn_tactic.cpp
@@ -3,11 +3,11 @@ Copyright (c) 2012 Microsoft Corporation
 
 Module Name:
 
-    pdr_tactic.h
+    horn_tactic.h
 
 Abstract:
 
-    PDR as a tactic to solve Horn clauses.
+    HORN as a tactic to solve Horn clauses.
 
 Author:
 
@@ -19,10 +19,10 @@ Revision History:
 #include"tactical.h"
 #include"model_converter.h"
 #include"proof_converter.h"
-#include"pdr_tactic.h"
+#include"horn_tactic.h"
 #include"dl_context.h"
 
-class pdr_tactic : public tactic {
+class horn_tactic : public tactic {
     struct imp {
         ast_manager&             m;
         datalog::context         m_ctx;
@@ -139,7 +139,7 @@ class pdr_tactic : public tactic {
                         expr_dependency_ref & core) {
             SASSERT(g->is_well_sorted());
             mc = 0; pc = 0; core = 0;
-            tactic_report report("pdr", *g);
+            tactic_report report("horn", *g);
             bool produce_models = g->models_enabled();
             bool produce_proofs = g->proofs_enabled();
 
@@ -210,7 +210,7 @@ class pdr_tactic : public tactic {
                 // subgoal is unchanged.
                 break;    
             }
-            TRACE("pdr", g->display(tout););
+            TRACE("horn", g->display(tout););
             SASSERT(g->is_well_sorted());
         }
     };
@@ -218,16 +218,16 @@ class pdr_tactic : public tactic {
     params_ref m_params;
     imp *      m_imp;
 public:
-    pdr_tactic(ast_manager & m, params_ref const & p):
+    horn_tactic(ast_manager & m, params_ref const & p):
         m_params(p) {
         m_imp = alloc(imp, m, p);
     }
 
     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);
     }
 
@@ -281,7 +281,7 @@ protected:
     }
 };
 
-tactic * mk_pdr_tactic(ast_manager & m, params_ref const & p) {
-    return clean(alloc(pdr_tactic, m, p));
+tactic * mk_horn_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(horn_tactic, m, p));
 }
 
diff --git a/src/muz_qe/pdr_tactic.h b/src/muz_qe/horn_tactic.h
similarity index 53%
rename from src/muz_qe/pdr_tactic.h
rename to src/muz_qe/horn_tactic.h
index 5a315152a..7f56a77ba 100644
--- a/src/muz_qe/pdr_tactic.h
+++ b/src/muz_qe/horn_tactic.h
@@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation
 
 Module Name:
 
-    pdr_tactic.h
+    horn_tactic.h
 
 Abstract:
 
@@ -16,15 +16,15 @@ Author:
 Revision History:
 
 --*/
-#ifndef _PDR_TACTIC_H_
-#define _PDR_TACTIC_H_
+#ifndef _HORN_TACTIC_H_
+#define _HORN_TACTIC_H_
 
 #include"params.h"
 class ast_manager;
 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
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index eb0534eea..4cf530b1e 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -33,7 +33,7 @@ Notes:
 #include"default_tactic.h"
 #include"ufbv_tactic.h"
 #include"qffpa_tactic.h"
-#include"pdr_tactic.h"
+#include"horn_tactic.h"
 #include"smt_solver.h"
 
 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(qffpa_fct, mk_qffpa_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) {
     s->set_default_tactic(alloc(default_fct));