Some clean-up, post bv-merge.

Add abc to build id and fix static building.

Add abc to --show-config output and Configuration class API.

Add ability to select abc source path.

Fix arch_flags for abc.

7 files changed, 38 insertions, 23 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 34fa20c1d..9531db0ce 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -433,6 +433,11 @@ if CVC4_USE_GLPK
 libcvc4_la_LIBADD += $(GLPK_LIBS)
 endif
 
+if CVC4_USE_ABC
+libcvc4_la_LIBADD += $(ABC_LIBS)
+libcvc4_la_LDFLAGS += $(ABC_LDFLAGS)
+endif
+
 BUILT_SOURCES = \
 	theory/rewriter_tables.h \
 	theory/theory_traits.h \
diff --git a/src/main/options_handlers.h b/src/main/options_handlers.h
index 7723dcb33..ee16af2f2 100644
--- a/src/main/options_handlers.h
+++ b/src/main/options_handlers.h
@@ -65,8 +65,9 @@ inline void showConfiguration(std::string option, SmtEngine* smt) {
   printf("\n");
   printf("cudd       : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no");
   printf("cln        : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no");
-  printf("glpk       : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no");
   printf("gmp        : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no");
+  printf("glpk       : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no");
+  printf("abc        : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no");
   printf("tls        : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no");
   exit(0);
 }
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp
index a5fe46d27..ebf36b0cd 100644
--- a/src/main/portfolio.cpp
+++ b/src/main/portfolio.cpp
@@ -95,7 +95,7 @@ std::pair<int, S> runPortfolio(int numThreads,
   for(int t = 0; t < numThreads; ++t) {
     if(optionWaitToJoin) {
       threads[t].join();
-    } 
+    }
   }
 
   std::pair<int, S> retval(global_winner, threads_returnValue[global_winner]);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b71969d15..6ab25ee57 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -367,9 +367,9 @@ private:
   void bvToBool();
 
   // Abstract common structure over small domains to UF
-  // return true if changes were made. 
-  void bvAbstraction(); 
-  
+  // return true if changes were made.
+  void bvAbstraction();
+
   // Simplify ITE structure
   bool simpITE();
 
@@ -1085,7 +1085,7 @@ void SmtEngine::setDefaults() {
     Notice() << "SmtEngine: turning off incremental to support eager bit-blasting" << endl;
     setOption("incremental", SExpr("false"));
   }
-  
+
   if (! options::bvEagerExplanations.wasSetByUser() &&
       d_logic.isTheoryEnabled(THEORY_ARRAY) &&
       d_logic.isTheoryEnabled(THEORY_BV)) {
@@ -1093,8 +1093,6 @@ void SmtEngine::setDefaults() {
     options::bvEagerExplanations.set(true);
   }
 
-  
-  
   // Turn on arith rewrite equalities only for pure arithmetic
   if(! options::arithRewriteEq.wasSetByUser()) {
     bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified();
@@ -2006,11 +2004,11 @@ void SmtEnginePrivate::bvAbstraction() {
     d_assertionsToPreprocess[i] = Rewriter::rewrite(new_assertions[i]);
   }
   // if we are using the lazy solver and the abstraction
-  // applies, then UF symbols were introduced 
+  // applies, then UF symbols were introduced
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY &&
       changed) {
     LogicRequest req(d_smt);
-    req.widenLogic(THEORY_UF); 
+    req.widenLogic(THEORY_UF);
   }
 }
 
@@ -2577,7 +2575,7 @@ bool SmtEnginePrivate::simplifyAssertions()
 
     // before ppRewrite check if only core theory for BV theory
     d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertionsToCheck);
-    
+
     // Theory preprocessing
     if (d_smt.d_earlyTheoryPP) {
       Chat() << "...doing early theory preprocessing..." << endl;
@@ -2870,18 +2868,17 @@ void SmtEnginePrivate::processAssertions() {
 
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
-  
+
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
       !d_smt.d_logic.isPure(THEORY_BV)) {
     throw ModalException("Eager bit-blasting does not currently support theory combination. "
                          "Note that in a QF_BV problem UF symbols can be introduced for division. "
-                         "Try --bv-div-zero-const to interpret division by zero as a constant."); 
+                         "Try --bv-div-zero-const to interpret division by zero as a constant.");
   }
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertionsToPreprocess); 
+    d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertionsToPreprocess);
   }
-  
 
   if ( options::bvAbstraction() &&
       !options::incrementalSolving()) {
@@ -2889,7 +2886,7 @@ void SmtEnginePrivate::processAssertions() {
     bvAbstraction();
     dumpAssertions("post-bv-abstraction", d_assertionsToPreprocess);
   }
-  
+
   dumpAssertions("pre-boolean-terms", d_assertionsToPreprocess);
   {
     Chat() << "rewriting Boolean terms..." << endl;
@@ -2952,7 +2949,7 @@ void SmtEnginePrivate::processAssertions() {
     bvToBool();
     dumpAssertions("post-bv-to-bool", d_assertionsToPreprocess);
   }
-  
+
   if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
     dumpAssertions("pre-strings-pp", d_assertionsToPreprocess);
     CVC4::theory::strings::StringsPreprocess sp;
@@ -3174,10 +3171,10 @@ void SmtEnginePrivate::processAssertions() {
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) {
       Node eager_atom = NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM, d_assertionsToCheck[i]);
-      d_assertionsToCheck[i] = eager_atom; 
+      d_assertionsToCheck[i] = eager_atom;
     }
   }
-  
+
   // Push the formula to decision engine
   if(noConflict) {
     Chat() << "pushing to decision engine..." << endl;
@@ -3191,6 +3188,7 @@ void SmtEnginePrivate::processAssertions() {
 
   dumpAssertions("post-everything", d_assertionsToCheck);
 
+  // Push the formula to SAT
   {
     Chat() << "converting to CNF..." << endl;
     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime);
@@ -3198,7 +3196,6 @@ void SmtEnginePrivate::processAssertions() {
       d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]);
     }
   }
-  
 
   d_assertionsProcessed = true;
 
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 0d22325e7..05f5c7678 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): Liana Hadarean, Tim King, ACSYS, Christopher L. Conway, Dejan Jovanovic, Francois Bobot
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -125,6 +125,10 @@ bool Configuration::isBuiltWithGlpk() {
   return IS_GLPK_BUILD;
 }
 
+bool Configuration::isBuiltWithAbc() {
+  return IS_ABC_BUILD;
+}
+
 bool Configuration::isBuiltWithCudd() {
   return false;
 }
diff --git a/src/util/configuration.h b/src/util/configuration.h
index 696b67715..c6562b3e6 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -5,7 +5,7 @@
  ** Major contributors: none
  ** Minor contributors (to current version): ACSYS, Liana Hadarean, Tim King, Francois Bobot
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -91,6 +91,8 @@ public:
 
   static bool isBuiltWithGlpk();
 
+  static bool isBuiltWithAbc();
+
   static bool isBuiltWithReadline();
 
   static bool isBuiltWithCudd();
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index 07ab4b17e..631a323d3 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -5,7 +5,7 @@
  ** Major contributors: ACSYS, Morgan Deters
  ** Minor contributors (to current version): Liana Hadarean, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -107,6 +107,12 @@ namespace CVC4 {
 #  define IS_GLPK_BUILD false
 #endif /* CVC4_USE_GLPK */
 
+#if CVC4_USE_ABC
+#  define IS_ABC_BUILD true
+#else /* CVC4_USE_ABC */
+#  define IS_ABC_BUILD false
+#endif /* CVC4_USE_ABC */
+
 #ifdef HAVE_LIBREADLINE
 #  define IS_READLINE_BUILD true
 #else /* HAVE_LIBREADLINE */