Adds a command line configuration option that is saved into a map. So that you can...

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 99c235e8c37d47fffc26ff43a10d62c108d5c8c5..fd73c53c8b568bfc7feaa1bc6b600730421f27c5 100644 (file)
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -9,8 +9,13 @@
 #ifndef UDEFFLAGS_H
 #define UDEFFLAGS_H
 
+#include <map>
+#include <string>
+#include <assert.h>
+#include <iostream>
 namespace BEEV
 {
+       using std::string;
 
   /******************************************************************
    * Struct UserDefFlags:
@@ -133,10 +138,44 @@ namespace BEEV
 
     enum SATSolvers solver_to_use;
 
+    std::map<string,string> 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<string,string>::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 76726d7348975d3f673e016a802bab92fe0c862e..d44dd6b1cc09918336dbfcf7c1e77b369890ae0d 100644 (file)
--- 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 10e46b75f439b9e6f56976d87e7b36d1c865edcd..7f1a45e034f0c509f091083341ea0ec1f05dffc8 100644 (file)
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -1462,14 +1462,6 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::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 <class BBNode, class BBNodeManagerT>
 BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBMult(const BBNodeVec& _x, const BBNodeVec& _y,
@@ -1485,28 +1477,27 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBMult(const BBNodeVec& _x, const B
         y = _x;
       }
 
+         string mv = uf->get("multiplication_variant","3");
+
       const int bitWidth = x.size();
+      stack<BBNode> products[bitWidth];
 
-      if (multiplication_variant1) {
-              //cout << "v1";
+      if (mv == "1") {
+              //cerr << "v1";
               return mult_normal(x, y, support);
       }
-
-      stack<BBNode> 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<BBNode,BBNodeManagerT>::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<BBNode,BBNodeManagerT>::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 a78d716760f19115645b550e322c3c81d57761e2..e37f466021718e21d8f8e740976deb84b36df2d1 100644 (file)
--- 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 9954dc3ad5a8222c8798fb4e34de6ed642574bfc..42dc48eccd729432b257790fb3c31b7e9536b479 100644 (file)
--- 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<ASTNode,BBNodeManagerASTNode> BB(&nm,&simp, bm->defaultNodeFactory);
+        BitBlaster<ASTNode,BBNodeManagerASTNode> BB(&nm,&simp, bm->defaultNodeFactory,&bm->UserFlags);
        BBFormula = BB.BBForm(input);
     }