basic fixes for sets translator, separate binaries

diff --git a/examples/sets-translate/Makefile.am b/examples/sets-translate/Makefile.am
index 40b79e998218d83e325fac3ef7ef63043476384d..720e565975651647863209411496073a6a0c7178 100644 (file)
--- a/examples/sets-translate/Makefile.am
+++ b/examples/sets-translate/Makefile.am
@@ -4,16 +4,25 @@ AM_CXXFLAGS = -Wall
 AM_CFLAGS = -Wall
 
 noinst_PROGRAMS = \
-       sets_translate  
+       sets2arrays \
+       sets2axioms
 
 noinst_DATA =
 
-sets_translate_SOURCES = \
+sets2arrays_SOURCES = \
        sets_translate.cpp
-sets_translate_LDADD = \
+sets2arrays_LDADD = \
        @builddir@/../../src/parser/libcvc4parser.la \
        @builddir@/../../src/libcvc4.la
 
+sets2axioms_SOURCES = \
+       sets_translate.cpp
+sets2axioms_LDADD = \
+       @builddir@/../../src/parser/libcvc4parser.la \
+       @builddir@/../../src/libcvc4.la
+sets2axioms_CXXFLAGS = \
+       -DENABLE_AXIOMS
+
 # for installation
 examplesdir = $(docdir)/$(subdir)
 examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST)

diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index dbc7100c0f6e918a7dc16565b4fa9dc85cf039ce..e23b7cec25d4b3a3a8006c1b78ab678934c398ac 100644 (file)
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -37,7 +37,11 @@ using namespace CVC4::options;
 
 bool nonsense(char c) { return !isalnum(c); } 
 
+#ifdef ENABLE_AXIOMS
 const bool enableAxioms = true;
+#else
+const bool enableAxioms = false;
+#endif
 
 string setaxioms[] = {
   "(declare-fun inHOLDA (HOLDB (Set HOLDB)) Bool)",
@@ -245,7 +249,7 @@ int main(int argc, char* argv[])
 
     // Get the filename 
     string input;
-    if(argv > 0) input = (argv[1]);
+    if(argc > 1) input = string(argv[1]);
     else input = "<stdin>";
 
     // Create the expression manager
@@ -259,6 +263,7 @@ int main(int argc, char* argv[])
   
     // Create the parser
     ParserBuilder parserBuilder(&exprManager, input, options);
+    if(input == "<stdin>") parserBuilder.withStreamInput(cin);
     Parser* parser = parserBuilder.build();
   
     // Variables and assertions
@@ -289,10 +294,19 @@ int main(int argc, char* argv[])
          return 0;
        }
         logicinfo = logicinfo.getUnlockedCopy();
-        logicinfo.disableTheory(theory::THEORY_SETS);
-        logicinfo.enableTheory(theory::THEORY_ARRAY);
-        logicinfo.lock();
-        // cout << SetBenchmarkLogicCommand(logicinfo.getLogicString()) << endl;
+        if(enableAxioms) {
+          logicinfo.enableQuantifiers();
+          logicinfo.lock();
+          if(!logicinfo.hasEverything()) {
+            (logicinfo = logicinfo.getUnlockedCopy()).disableTheory(theory::THEORY_SETS);
+            logicinfo.lock();
+            cout << SetBenchmarkLogicCommand(logicinfo.getLogicString()) << endl;
+          }
+        } else {
+          logicinfo.enableTheory(theory::THEORY_ARRAY);
+          // we print logic string only for Quantifiers, for Z3 stuff
+          // we don't set the logic
+        }
 
         delete cmd;
         continue;