Refactor. Move the code that goes to CNF via ASTNodes to it's own directory.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1087 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index 84085deaebea66038b7ebc98762c3f863aa2436c..24379658705a2396cb4cc05dde45fee4a7c38bbd 100644 (file)
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -15,7 +15,7 @@
 #include "../STPManager/STPManager.h"
 #include "../simplifier/bvsolver.h"
 #include "../simplifier/simplifier.h"
-#include "../to-sat/ToSAT.h"
+#include "../to-sat/ASTNode/ToSAT.h"
 #include "../parser/LetMgr.h"
 #include "../absrefine_counterexample/AbsRefine_CounterExample.h"
 

diff --git a/src/to-sat/BBNodeManagerASTNode.h b/src/to-sat/ASTNode/BBNodeManagerASTNode.h
similarity index 88%
rename from src/to-sat/BBNodeManagerASTNode.h
rename to src/to-sat/ASTNode/BBNodeManagerASTNode.h
index 8011a418157dea196e7911d3c1a711e666e8291a..3ec50d3f8bd528bb7eebd191292978e3635617ac 100644 (file)
--- a/src/to-sat/BBNodeManagerASTNode.h
+++ b/src/to-sat/ASTNode/BBNodeManagerASTNode.h
@@ -1,7 +1,10 @@
 #ifndef BBNodeManager_H_
 #define BBNodeManager_H_
 
-#include "../STPManager/STPManager.h"
+// We can bitblast either via ASTNodes, or via AIG nodes. The AIG nodes use less memory, and produce better CNFs. The ASTNodes are the
+// traditional way of doing it.
+
+#include "../../STPManager/STPManager.h"
 
 namespace BEEV {
 class ASTNode;

diff --git a/src/to-sat/ClauseList.cpp b/src/to-sat/ASTNode/ClauseList.cpp
similarity index 96%
rename from src/to-sat/ClauseList.cpp
rename to src/to-sat/ASTNode/ClauseList.cpp
index eef4a78452ee122389d94e03de0f2843070011fa..774ca1f82a49535714976c86fb8c46c1f8b7fc27 100644 (file)
--- a/src/to-sat/ClauseList.cpp
+++ b/src/to-sat/ASTNode/ClauseList.cpp
@@ -1,5 +1,5 @@
 #include "ClauseList.h"
-#include "../AST/AST.h"
+#include "../../AST/AST.h"
 
 namespace BEEV
 {

diff --git a/src/to-sat/ClauseList.h b/src/to-sat/ASTNode/ClauseList.h
similarity index 99%
rename from src/to-sat/ClauseList.h
rename to src/to-sat/ASTNode/ClauseList.h
index 074801b8c3e26eb43555a1203a2db92f3ea2dfbf..0cfe477ebb3aef162f55cf2bf5e240d0e39d226d 100644 (file)
--- a/src/to-sat/ClauseList.h
+++ b/src/to-sat/ASTNode/ClauseList.h
@@ -1,7 +1,7 @@
 #ifndef CLAUSELIST_H_
 #define CLAUSELIST_H_
 
-#include "../AST/AST.h"
+#include "../../AST/AST.h"
 #include <cassert>
 
 namespace BEEV

diff --git a/src/to-sat/SimpBool.cpp b/src/to-sat/ASTNode/SimpBool.cpp
similarity index 99%
rename from src/to-sat/SimpBool.cpp
rename to src/to-sat/ASTNode/SimpBool.cpp
index 4184b75af284aa65eb162a4adfad5a94b0a46b35..3b04c854bd7a243c18b14d7a319175c350d1ec6a 100644 (file)
--- a/src/to-sat/SimpBool.cpp
+++ b/src/to-sat/ASTNode/SimpBool.cpp
@@ -13,8 +13,8 @@
 static bool _trace_simpbool = 0;
 static bool _disable_simpbool = 0;
 
-#include "../AST/AST.h"
-#include "../STPManager/STPManager.h"
+#include "../../AST/AST.h"
+#include "../../STPManager/STPManager.h"
 
 // SMTLIB experimental hack.  Try allocating a single stack here for
 // children to reduce growing of vectors.  BEEV::ASTVec child_stack;

diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ASTNode/ToCNF.cpp
similarity index 99%
rename from src/to-sat/ToCNF.cpp
rename to src/to-sat/ASTNode/ToCNF.cpp
index 6342f5ac95747a3ad1c09a03c95e9ce218f86c77..dde980fb0cea947ee1dfa5e6f0a97d08c9ddaa42 100644 (file)
--- a/src/to-sat/ToCNF.cpp
+++ b/src/to-sat/ASTNode/ToCNF.cpp
@@ -7,8 +7,8 @@
  * LICENSE: Please view LICENSE file in the home dir of this Program
  ********************************************************************/
 
-#include "../AST/AST.h"
-#include "../STPManager/STPManager.h"
+#include "../../AST/AST.h"
+#include "../../STPManager/STPManager.h"
 #include "ToCNF.h"
 
 namespace BEEV

diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ASTNode/ToCNF.h
similarity index 99%
rename from src/to-sat/ToCNF.h
rename to src/to-sat/ASTNode/ToCNF.h
index 7c9d25d74f67ef3a9d81924538507a7e706722a3..cb76a974c75e22ea2e386db51a5f695951fb91ee 100644 (file)
--- a/src/to-sat/ToCNF.h
+++ b/src/to-sat/ASTNode/ToCNF.h
@@ -12,8 +12,8 @@
 
 #include <cmath>
 #include <cassert>
-#include "../AST/AST.h"
-#include "../STPManager/STPManager.h"
+#include "../../AST/AST.h"
+#include "../../STPManager/STPManager.h"
 #include "ClauseList.h"
 
 namespace BEEV

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ASTNode/ToSAT.cpp
similarity index 99%
rename from src/to-sat/ToSAT.cpp
rename to src/to-sat/ASTNode/ToSAT.cpp
index 07e16277c6747a004b20c7dacebb8a1258b8e306..33771892b06ca600a6e9ce361194901952690c0a 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ASTNode/ToSAT.cpp
@@ -7,12 +7,12 @@
  * LICENSE: Please view LICENSE file in the home dir of this Program
  ********************************************************************/
 #include "ToSAT.h"
-#include "BitBlaster.h"
-#include "../printer/printers.h"
+#include "../BitBlaster.h"
+#include "../../printer/printers.h"
 #include <iostream>
 #include <fstream>
 #include "BBNodeManagerASTNode.h"
-#include "../STPManager/UserDefinedFlags.h"
+#include "../../STPManager/UserDefinedFlags.h"
 
 namespace BEEV
 {

diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ASTNode/ToSAT.h
similarity index 97%
rename from src/to-sat/ToSAT.h
rename to src/to-sat/ASTNode/ToSAT.h
index 474e372e0e5d70f806454effbcbbd6440dec0447..acbba5ea2148a86b0f43fbf71479de6a639fad7f 100644 (file)
--- a/src/to-sat/ToSAT.h
+++ b/src/to-sat/ASTNode/ToSAT.h
@@ -12,9 +12,9 @@
 
 #include "ToCNF.h"
 
-#include "../AST/AST.h"
-#include "../STPManager/STPManager.h"
-#include "ToSATBase.h"
+#include "../../AST/AST.h"
+#include "../../STPManager/STPManager.h"
+#include "../ToSATBase.h"
 
 namespace BEEV
 {

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 7f1a45e034f0c509f091083341ea0ec1f05dffc8..d7a4cb0b9007aeec8c1aa38a53834333c00d3546 100644 (file)
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -11,7 +11,7 @@
 #include <cassert>
 #include "BitBlaster.h"
 #include "AIG/BBNodeManagerAIG.h"
-#include "BBNodeManagerASTNode.h"
+#include "ASTNode/BBNodeManagerASTNode.h"
 #include "../simplifier/constantBitP/FixedBits.h"
 #include "../simplifier/constantBitP/ConstantBitPropagation.h"
 #include "../simplifier/constantBitP/NodeToFixedBitsMap.h"

diff --git a/src/to-sat/Makefile b/src/to-sat/Makefile
index 2d7a27b2ac43a32ede48610b0368a78399058a4f..05b33387c2d9539e8e3fd64e37edc47c4138b996 100644 (file)
--- a/src/to-sat/Makefile
+++ b/src/to-sat/Makefile
@@ -3,6 +3,7 @@ include $(TOP)/scripts/Makefile.common
 
 SRCS = $(wildcard *.cpp)
 SRCS += $(wildcard AIG/*.cpp)
+SRCS += $(wildcard ASTNode/*.cpp)
 OBJS = $(SRCS:.cpp=.o)
 
 CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE)
@@ -13,7 +14,7 @@ libtosat.a:   $(OBJS) depend
 
 .PHONY: clean
 clean: 
-               rm -rf *.o *~ *.a .#* depend AIG/*.o
+               rm -rf *.o *~ *.a .#* depend AIG/*.o ASTNode/*.o
 
 depend: $(SRCS)
        @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@