From 1010bd11b2610e11da3bdd7e0b7b99a9f7fe181d Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 23 Jan 2011 13:08:12 +0000 Subject: [PATCH] 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 --- src/STPManager/STP.h | 2 +- src/to-sat/{ => ASTNode}/BBNodeManagerASTNode.h | 5 ++++- src/to-sat/{ => ASTNode}/ClauseList.cpp | 2 +- src/to-sat/{ => ASTNode}/ClauseList.h | 2 +- src/to-sat/{ => ASTNode}/SimpBool.cpp | 4 ++-- src/to-sat/{ => ASTNode}/ToCNF.cpp | 4 ++-- src/to-sat/{ => ASTNode}/ToCNF.h | 4 ++-- src/to-sat/{ => ASTNode}/ToSAT.cpp | 6 +++--- src/to-sat/{ => ASTNode}/ToSAT.h | 6 +++--- src/to-sat/BitBlaster.cpp | 2 +- src/to-sat/Makefile | 3 ++- 11 files changed, 22 insertions(+), 18 deletions(-) rename src/to-sat/{ => ASTNode}/BBNodeManagerASTNode.h (88%) rename src/to-sat/{ => ASTNode}/ClauseList.cpp (96%) rename src/to-sat/{ => ASTNode}/ClauseList.h (99%) rename src/to-sat/{ => ASTNode}/SimpBool.cpp (99%) rename src/to-sat/{ => ASTNode}/ToCNF.cpp (99%) rename src/to-sat/{ => ASTNode}/ToCNF.h (99%) rename src/to-sat/{ => ASTNode}/ToSAT.cpp (99%) rename src/to-sat/{ => ASTNode}/ToSAT.h (97%) diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h index 84085de..2437965 100644 --- 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 8011a41..3ec50d3 100644 --- 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 eef4a78..774ca1f 100644 --- 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 074801b..0cfe477 100644 --- 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 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 4184b75..3b04c85 100644 --- 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 6342f5a..dde980f 100644 --- 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 7c9d25d..cb76a97 100644 --- a/src/to-sat/ToCNF.h +++ b/src/to-sat/ASTNode/ToCNF.h @@ -12,8 +12,8 @@ #include #include -#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 07e1627..3377189 100644 --- 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 #include #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 474e372..acbba5e 100644 --- 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 7f1a45e..d7a4cb0 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -11,7 +11,7 @@ #include #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 2d7a27b..05b3338 100644 --- 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) > $@ -- 2.47.3