Sets translate, and other short fixes

- $ is a simple symbol is smt2.
- ever found yourself counting in kind.h? no longer.
- expose parser "logic is set" state for smt/smt2 (any better way?)
- a more helpful assertion message in smt_engine

4 files changed, 312 insertions, 1 deletions

diff --git a/examples/Makefile.am b/examples/Makefile.am
index 940af06ff..0f5c7db98 100644
--- a/examples/Makefile.am
+++ b/examples/Makefile.am
@@ -1,14 +1,16 @@
-SUBDIRS = nra-translate hashsmt api .
+SUBDIRS = nra-translate sets-translate hashsmt api .
 
 AM_CPPFLAGS = \
 	-I@srcdir@/../src/include -I@srcdir@/../src -I@builddir@/../src $(ANTLR_INCLUDES)
 AM_CXXFLAGS = -Wall
 AM_CFLAGS = -Wall
 
+
 noinst_PROGRAMS = \
 	simple_vc_cxx \
 	translator
 
+
 if CVC4_BUILD_LIBCOMPAT
 noinst_PROGRAMS += \
 	simple_vc_compat_cxx
diff --git a/examples/sets-translate/Makefile b/examples/sets-translate/Makefile
new file mode 100644
index 000000000..8efe0c48e
--- /dev/null
+++ b/examples/sets-translate/Makefile
@@ -0,0 +1,4 @@
+topdir = ../..
+srcdir = examples/sets-translate
+
+include $(topdir)/Makefile.subdir
diff --git a/examples/sets-translate/Makefile.am b/examples/sets-translate/Makefile.am
new file mode 100644
index 000000000..40b79e998
--- /dev/null
+++ b/examples/sets-translate/Makefile.am
@@ -0,0 +1,19 @@
+AM_CPPFLAGS = \
+	-I@srcdir@/../../src/include -I@srcdir@/../../src -I@builddir@/../../src $(ANTLR_INCLUDES)
+AM_CXXFLAGS = -Wall
+AM_CFLAGS = -Wall
+
+noinst_PROGRAMS = \
+	sets_translate	
+
+noinst_DATA =
+
+sets_translate_SOURCES = \
+	sets_translate.cpp
+sets_translate_LDADD = \
+	@builddir@/../../src/parser/libcvc4parser.la \
+	@builddir@/../../src/libcvc4.la
+
+# 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
new file mode 100644
index 000000000..6cf2b61e2
--- /dev/null
+++ b/examples/sets-translate/sets_translate.cpp
@@ -0,0 +1,286 @@
+/*********************                                                        */
+/*! \file sets-translate.cpp
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: None
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** 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
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include <string>
+#include <iostream>
+#include <typeinfo>
+#include <cassert>
+#include <vector>
+
+
+#include "options/options.h"
+#include "expr/expr.h"
+#include "theory/logic_info.h"
+#include "expr/command.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::parser;
+using namespace CVC4::options;
+
+bool nonsense(char c) { return !isalnum(c); } 
+
+class Mapper {
+  set< Type > setTypes;
+  map< Type, Type > mapTypes;
+  map< pair<Type, Kind>, Expr > setoperators;
+  hash_map< Expr, Expr, ExprHashFunction > substitutions;
+  ostringstream sout;
+  ExprManager* em;
+
+  Expr add(SetType t, Expr e) {
+
+    if(setTypes.find(t) == setTypes.end() ) {
+      // mark as processed
+      setTypes.insert(t);
+
+      Type elementType = t.getElementType();
+      string elementTypeAsString = elementType.toString();
+      remove_if(elementTypeAsString.begin(), elementTypeAsString.end(), nonsense);
+
+      // define-sort
+      ostringstream oss_name;
+      oss_name << Expr::setlanguage(language::output::LANG_SMTLIB_V2)
+               << "(Set " << elementType << ")";
+      string name = oss_name.str();
+      Type newt = em->mkArrayType(t.getElementType(), em->booleanType());
+      mapTypes[t] = newt;
+
+      // diffent types
+      vector<Type> t_t;
+      t_t.push_back(t);
+      t_t.push_back(t);
+      vector<Type> elet_t;
+      elet_t.push_back(elementType);
+      elet_t.push_back(t);
+
+      sout << "(define-fun emptyset" << elementTypeAsString << "    "
+           << " ()"
+           << " " << name
+           << " ( (as const " << name << ") false ) )" << endl;
+      setoperators[ make_pair(t, kind::EMPTYSET) ] =
+        em->mkVar( std::string("emptyset") + elementTypeAsString,
+                   t);
+
+      sout << "(define-fun setenum" << elementTypeAsString << "     "
+           << " ( (x " << elementType << ") )"
+           << " " << name << ""
+           << " (store emptyset" << elementTypeAsString << " x true) )" << endl;
+      setoperators[ make_pair(t, kind::SET_SINGLETON) ] =
+        em->mkVar( std::string("setenum") + elementTypeAsString,
+                   em->mkFunctionType( elementType, t ) );
+
+      sout << "(define-fun union" << elementTypeAsString << "       "
+           << " ( (s1 " << name << ") (s2 " << name << ") )"
+           << " " << name << ""
+           << " ((_ map or) s1 s2))" << endl;
+      setoperators[ make_pair(t, kind::UNION) ] =
+        em->mkVar( std::string("union") + elementTypeAsString,
+                   em->mkFunctionType( t_t, t ) );
+
+      sout << "(define-fun intersection" << elementTypeAsString << ""
+           << " ( (s1 " << name << ") (s2 " << name << ") )"
+           << " " << name << ""
+           << " ((_ map and) s1 s2))" << endl;
+      setoperators[ make_pair(t, kind::INTERSECTION) ] =
+        em->mkVar( std::string("intersection") + elementTypeAsString,
+                   em->mkFunctionType( t_t, t ) );
+
+      sout << "(define-fun setminus" << elementTypeAsString << "    "
+           << " ( (s1 " << name << ") (s2 " << name << ") )"
+           << " " << name << ""
+           << " (intersection" << elementTypeAsString << " s1 ((_ map not) s2)))" << endl;
+      setoperators[ make_pair(t, kind::SETMINUS) ] =
+        em->mkVar( std::string("setminus") + elementTypeAsString,
+                   em->mkFunctionType( t_t, t ) );
+
+      sout << "(define-fun in" << elementTypeAsString << "          "
+           << " ( (x " << elementType << ")" << " (s " << name << "))"
+           << " Bool"
+           << " (select s x) )" << endl;
+      setoperators[ make_pair(t, kind::MEMBER) ] =
+        em->mkVar( std::string("in") + elementTypeAsString,
+                   em->mkPredicateType( elet_t ) );
+
+      sout << "(define-fun subseteq" << elementTypeAsString << "    "
+           << " ( (s1 " << name << ") (s2 " << name << ") )"
+           << " Bool"
+           <<" (= emptyset" << elementTypeAsString << " (setminus" << elementTypeAsString << " s1 s2)) )" << endl;
+      setoperators[ make_pair(t, kind::SUBSET) ] =
+        em->mkVar( std::string("subseteq") + elementTypeAsString,
+                   em->mkPredicateType( t_t ) );
+
+    }
+    Expr ret;
+    if(e.getKind() == kind::EMPTYSET) {
+      ret = setoperators[ make_pair(t, e.getKind()) ];
+    } else {
+      vector<Expr> children = e.getChildren();
+      children.insert(children.begin(), setoperators[ make_pair(t, e.getKind()) ]);
+      ret = em->mkExpr(kind::APPLY, children);
+    }
+    // cout << "returning " << ret  << endl;
+    return ret;
+  }
+
+public:
+  Mapper(ExprManager* e) : em(e) {
+    sout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
+  }
+
+  void defineSetSort() {
+    if(setTypes.empty()) {
+      cout << "(define-sort Set (X) (Array X Bool) )" << endl;
+    }
+  }
+
+
+  Expr collectSortsExpr(Expr e)
+  {
+    Expr old_e = e;
+    for(unsigned i = 0; i < e.getNumChildren(); ++i) {
+      collectSortsExpr(e[i]);
+    }
+    e = e.substitute(substitutions);
+    if(theory::kindToTheoryId(e.getKind()) == theory::THEORY_SETS) {
+      SetType t = SetType(e.getType().isBoolean() ? e[1].getType() : e.getType());
+      substitutions[e] = add(t, e);
+      e = e.substitute(substitutions);
+    }
+    // cout << old_e << " => " << e << endl;
+    return e;
+  }
+
+  void dump() {
+    cout << sout.str();
+  }
+};
+
+
+int main(int argc, char* argv[]) 
+{
+
+  try {
+
+    // Get the filename 
+    string input;
+    if(argv > 0) input = (argv[1]);
+    else input = "<stdin>";
+
+    // Create the expression manager
+    Options options;
+    options.set(inputLanguage, language::input::LANG_SMTLIB_V2);
+    cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2);
+    ExprManager exprManager(options);
+
+    Mapper m(&exprManager);
+  
+    // Create the parser
+    ParserBuilder parserBuilder(&exprManager, input, options);
+    Parser* parser = parserBuilder.build();
+  
+    // Variables and assertions
+    vector<string> variables;
+    vector<string> info_tags;
+    vector<string> info_data;
+    vector<Expr> assertions;
+  
+    Command* cmd = NULL;
+    CommandSequence commandsSequence;
+    bool logicisset = false;
+
+    while ((cmd = parser->nextCommand())) {
+
+      // till logic is set, don't do any modifications
+      if(!parser->logicIsSet()) {
+        cout << (*cmd) << endl;
+        delete cmd;
+        continue;
+      }
+
+      // transform set-logic command, if there is one
+      SetBenchmarkLogicCommand* setlogic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd);
+      if(setlogic) {
+	LogicInfo logicinfo(setlogic->getLogic());
+	if(!logicinfo.isTheoryEnabled(theory::THEORY_SETS)) {
+	  cerr << "Sets theory not enabled. Stopping translation." << endl;
+	  return 0;
+	}
+        logicinfo = logicinfo.getUnlockedCopy();
+        logicinfo.disableTheory(theory::THEORY_SETS);
+        logicinfo.enableTheory(theory::THEORY_ARRAY);
+        logicinfo.lock();
+        // cout << SetBenchmarkLogicCommand(logicinfo.getLogicString()) << endl;
+
+        delete cmd;
+        continue;
+      }
+
+      // if we reach here, logic is set by now, so can define our sort
+      if( !logicisset ) {
+        logicisset = true;
+        m.defineSetSort();
+      }
+
+      // declare/define-sort commands are printed immediately
+      DeclareTypeCommand* declaresort = dynamic_cast<DeclareTypeCommand*>(cmd);
+      DefineTypeCommand* definesort = dynamic_cast<DefineTypeCommand*>(cmd);
+      if(declaresort || definesort) {
+        cout << *cmd << endl;
+        delete cmd;
+        continue;
+      }
+
+      // other commands are queued up, while replacing with new function symbols
+      AssertCommand* assert = dynamic_cast<AssertCommand*>(cmd);
+      DeclareFunctionCommand* declarefun = dynamic_cast<DeclareFunctionCommand*>(cmd);
+      DefineFunctionCommand* definefun = dynamic_cast<DefineFunctionCommand*>(cmd);
+
+      Command* new_cmd = NULL;
+      if(assert) {
+        Expr newexpr = m.collectSortsExpr(assert->getExpr());
+        new_cmd = new AssertCommand(newexpr);
+      } else if(declarefun) {
+        Expr newfunc = m.collectSortsExpr(declarefun->getFunction());
+        new_cmd = new DeclareFunctionCommand(declarefun->getSymbol(), newfunc, declarefun->getType());
+      } else if(definefun) {
+        Expr newfunc = m.collectSortsExpr(definefun->getFunction());
+        Expr newformula = m.collectSortsExpr(definefun->getFormula());
+        new_cmd = new DefineFunctionCommand(definefun->getSymbol(), newfunc, definefun->getFormals(), newformula);
+      }
+
+      if(new_cmd == NULL) {
+        commandsSequence.addCommand(cmd);
+      } else {
+        commandsSequence.addCommand(new_cmd);
+        delete cmd;
+      }
+
+    }
+
+    m.dump();
+    cout << commandsSequence;
+    
+  
+    // Get rid of the parser
+    //delete parser;
+  } catch (Exception& e) {
+    cerr << e << endl;
+  }
+}