From: trevor_hansen Date: Wed, 15 Dec 2010 07:34:49 +0000 (+0000) Subject: Adds a command line configuration option that is saved into a map. So that you can... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=147371a7062cf0d74adfc5f25514d959e907f813;p=francis%2Fstp.git Adds a command line configuration option that is saved into a map. So that you can do: --config_va=3 for instance. This will save va="3" into the config_options map. I'm intending to use this to allow more options to be controlled from the command line without having the hastle of creating new names for each of them. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1035 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h index 99c235e..fd73c53 100644 --- a/src/STPManager/UserDefinedFlags.h +++ b/src/STPManager/UserDefinedFlags.h @@ -9,8 +9,13 @@ #ifndef UDEFFLAGS_H #define UDEFFLAGS_H +#include +#include +#include +#include namespace BEEV { + using std::string; /****************************************************************** * Struct UserDefFlags: @@ -133,10 +138,44 @@ namespace BEEV enum SATSolvers solver_to_use; + std::map config_options; + + void set(string n, string v) + { + assert(n.size() > 0); + assert(v.size() > 0); + assert(config_options.find(n) == config_options.end()); + config_options[n] = v; + } + + string get(string n) + { + return get(n,""); + } + + string get(string n, string def) + { + if (config_options.empty()) + return def; + + string result; + std::map::iterator it = config_options.find(n); + if (it == config_options.end()) + result = def; + else + result = it->second; + + if (stats_flag) + std::cout << n << ":" << result << std::endl; + + return result; + } + //CONSTRUCTOR UserDefinedFlags() { - //collect statistics on certain functions + + //collect statistics on certain functions stats_flag = false; //print DAG nodes diff --git a/src/main/main.cpp b/src/main/main.cpp index 76726d7..d44dd6b 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -197,6 +197,28 @@ int main(int argc, char ** argv) { lookup.insert(make_pair(tolower("--SMTLIB1"),SMT_LIB1_FORMAT)); lookup.insert(make_pair(tolower("--disable-cbitp"),DISABLE_CBITP)); + if (!strncmp(argv[i],"--config_",strlen("--config_"))) + { + // Must contain an equals. + // Must contain a name >=1 character long. + // Must contain a value >=1 char. + string s(argv[i]); + size_t a = s.find("_"); + size_t b = s.find("="); + if (a== string::npos || b == string::npos || b < a || b==a+1 || b==s.length()-1) + { + fprintf(stderr,usage,prog); + cout << helpstring; + return -1; + break; + } + + string name = s.substr(a+1,b-a-1); + string value = s.substr(b+1); + + bm->UserFlags.set(name,value); + } + else switch(lookup[tolower(argv[i])]) { diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index 10e46b7..7f1a45e 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -1462,14 +1462,6 @@ BBNodeVec BitBlaster::mult_normal(const BBNodeVec& x, } -// ONLY SELECT ONE OF THESE! -const bool multiplication_variant1 = false; // multiplication with repeat addition. -const bool multiplication_variant2 = false; // multiplication with partial products. -const bool multiplication_variant3 = true; // multiplication with booth recoding. -const bool multiplication_variant4 = false; // multiplication via sorting networks. -const bool multiplication_variant5 = false; // Using bounds. - - // Multiply two bitblasted numbers template BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const BBNodeVec& _y, @@ -1485,28 +1477,27 @@ BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const B y = _x; } + string mv = uf->get("multiplication_variant","3"); + const int bitWidth = x.size(); + stack products[bitWidth]; - if (multiplication_variant1) { - //cout << "v1"; + if (mv == "1") { + //cerr << "v1"; return mult_normal(x, y, support); } - - stack products[bitWidth]; - - if (multiplication_variant2) { + else if (mv == "2") { //cout << "v2"; mult_allPairs(x, y, support,products); return buildAdditionNetworkResult(products,support, bitWidth); } - if (multiplication_variant3) { - //cout << "v3"; + else if (mv == "3") { + //cout << "v3" << endl; mult_Booth(_x, _y, support,n[0],n[1],products); return buildAdditionNetworkResult(products,support,bitWidth); } - - if (multiplication_variant4) + else if (mv == "4") { //cout << "v4"; mult_Booth(_x, _y, support,n[0],n[1],products); @@ -1520,8 +1511,7 @@ BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const B } return buildAdditionNetworkResult(products,support, bitWidth); } - - if (multiplication_variant5) + else if (mv == "5") { //cout << "v5"; if (!statsFound(n)) @@ -1533,8 +1523,8 @@ BBNodeVec BitBlaster::BBMult(const BBNodeVec& _x, const B mult_allPairs(x, y, support, products); return multWithBounds(n, products, support); } - - FatalError("sda44f"); + else + FatalError("sda44f"); } //====== diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h index a78d716..e37f466 100644 --- a/src/to-sat/BitBlaster.h +++ b/src/to-sat/BitBlaster.h @@ -186,9 +186,7 @@ public: uf = _uf; } - - - BitBlaster(BBNodeManagerT* bnm, Simplifier* _simp, NodeFactory *astNodeF) + BitBlaster(BBNodeManagerT* bnm, Simplifier* _simp, NodeFactory *astNodeF, UserDefinedFlags *_uf) { nf = bnm; BBTrue = nf->getTrue(); @@ -196,8 +194,8 @@ public: cb = NULL; simp = _simp; ASTNF = astNodeF; - uf = NULL; - } + uf = _uf; + } void ClearAllTables() diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 9954dc3..42dc48e 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -338,7 +338,7 @@ namespace BEEV { BBNodeManagerASTNode nm(bm); Simplifier simp(bm); - BitBlaster BB(&nm,&simp, bm->defaultNodeFactory); + BitBlaster BB(&nm,&simp, bm->defaultNodeFactory,&bm->UserFlags); BBFormula = BB.BBForm(input); }