From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 18 Jun 2014 19:51:57 +0000 (-0400)
Subject: basic fixes for sets translator, separate binaries
X-Git-Tag: cvc5-1.0.0~6758^2~7
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b56d4c02290f8a20bb0ff27d19920f7ce6f66576;p=cvc5.git

basic fixes for sets translator, separate binaries
---

diff --git a/examples/sets-translate/Makefile.am b/examples/sets-translate/Makefile.am
index 40b79e998..720e56597 100644
--- 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 dbc7100c0..e23b7cec2 100644
--- 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;