Merge pull request #26 from kbansal/sets

Sets

13 files changed, 153 insertions, 22 deletions

diff --git a/proofs/lfsc_checker/code.cpp b/proofs/lfsc_checker/code.cpp
index 34c6c133b..ee143a710 100644
--- a/proofs/lfsc_checker/code.cpp
+++ b/proofs/lfsc_checker/code.cpp
@@ -1141,7 +1141,7 @@ Expr *run_code(Expr *_e) {
     if (!r1)
       return NULL;
 
-    bool cond;
+    bool cond = true;
     if( r1->getclass() == INT_EXPR ){
       if( e->getop() == IFNEG )
         cond = mpz_sgn( ((IntExpr *)r1)->n )<0;
@@ -1244,7 +1244,7 @@ Expr *run_code(Expr *_e) {
     vector<Expr *> args;
     Expr *hd = scrut->collect_args(args);
     Expr **cases = &e->kids[1];
-    CExpr *c;
+    // CExpr *c;
     Expr *c_or_default;
     while ((c_or_default = *cases++)) {
 
@@ -1382,4 +1382,4 @@ int read_index()
     index = atoi( v.c_str() );
   }
   return index;
-}
\ No newline at end of file
+}
diff --git a/proofs/lfsc_checker/print_smt2.cpp b/proofs/lfsc_checker/print_smt2.cpp
index bf068c248..34cb00cc4 100644
--- a/proofs/lfsc_checker/print_smt2.cpp
+++ b/proofs/lfsc_checker/print_smt2.cpp
@@ -54,7 +54,7 @@ void print_smt2( Expr* p, std::ostream& s, short mode )
             s << " ";

             for( int a=0; a<(int)args.size(); a++ ){

               print_smt2( args[a], s, newMode );

-              if( a!=args.size()-1 )

+              if( a!=(int)args.size()-1 )

                 s << " ";

             }

             s << ")";

diff --git a/proofs/lfsc_checker/scccode.cpp b/proofs/lfsc_checker/scccode.cpp
index cff762a08..22f26ec88 100644
--- a/proofs/lfsc_checker/scccode.cpp
+++ b/proofs/lfsc_checker/scccode.cpp
@@ -99,11 +99,11 @@ Expr* f_litpol( Expr* l ){
    e3 = e_neg;
    e3->inc();
    if( e1==e2 ){
-      Expr* x = ((CExpr*)l->followDefs())->kids[1];
+      // Expr* x = ((CExpr*)l->followDefs())->kids[1];
       e0 = e_tt;
       e0->inc();
    }else if( e1==e3 ){
-      Expr* x = ((CExpr*)l->followDefs())->kids[1];
+      // Expr* x = ((CExpr*)l->followDefs())->kids[1];
       e0 = e_ff;
       e0->inc();
    }else{
diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h
index 3779f75c1..15813a774 100644
--- a/src/options/base_options_handlers.h
+++ b/src/options/base_options_handlers.h
@@ -100,7 +100,8 @@ inline InputLanguage stringToInputLanguage(std::string option, std::string optar
   Unreachable();
 }
 
-inline std::string suggestTags(char const* const* validTags, std::string inputTag)
+inline std::string suggestTags(char const* const* validTags, std::string inputTag,
+                               char const* const* additionalTags = NULL)
 {
   DidYouMean didYouMean;
 
@@ -108,6 +109,11 @@ inline std::string suggestTags(char const* const* validTags, std::string inputTa
   for(size_t i = 0; (opt = validTags[i]) != NULL; ++i) {
     didYouMean.addWord(validTags[i]);
   }
+  if(additionalTags != NULL) {
+    for(size_t i = 0; (opt = additionalTags[i]) != NULL; ++i) {
+      didYouMean.addWord(additionalTags[i]);
+    }
+  }
 
   return  didYouMean.getMatchAsString(inputTag);
 }
@@ -130,7 +136,7 @@ inline void addDebugTag(std::string option, std::string optarg, SmtEngine* smt)
        !Configuration::isTraceTag(optarg.c_str())) {
       throw OptionException(std::string("debug tag ") + optarg +
                             std::string(" not available.") +
-                            suggestTags(Configuration::getDebugTags(), optarg) );
+                            suggestTags(Configuration::getDebugTags(), optarg, Configuration::getTraceTags()) );
     }
   } else if(! Configuration::isDebugBuild()) {
     throw OptionException("debug tags not available in non-debug builds");
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index a16e7f899..39deb285a 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -570,7 +570,7 @@ std::string Options::suggestCommandLineOptions(const std::string& optionName) th
     didYouMean.addWord(std::string("--") + cmdlineOptions[i].name);
   }
 
-  return didYouMean.getMatchAsString(optionName);
+  return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('=')));
 }
 
 static const char* smtOptions[] = {
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 9d00cde7b..af96b50d0 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -190,6 +190,29 @@ void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
     return;
   }
 
+  /**
+   * Disequality propagation if element type is set
+   */
+  if(x.getType().isSet()) {
+    if(polarity) {
+      const CDTNodeList* l = d_termInfoManager->getNonMembers(S);
+      for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
+        TNode n = *it;
+        learnLiteral( /* atom = */ EQUAL(x, n),
+                      /* polarity = */ false,
+                      /* reason = */ AND( MEMBER(x, S), NOT( MEMBER(n, S)) ) );
+      }
+    } else {
+      const CDTNodeList* l = d_termInfoManager->getMembers(S);
+      for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
+        TNode n = *it;
+        learnLiteral( /* atom = */ EQUAL(x, n),
+                      /* polarity = */ false,
+                      /* reason = */ AND( NOT(MEMBER(x, S)), MEMBER(n, S)) );
+      }
+    }
+  }
+
   for(; !j.isFinished(); ++j) {
     TNode S = (*j);
     Node cur_atom = MEMBER(x, S);
@@ -227,7 +250,10 @@ void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
   Debug("sets-prop") << "[sets-prop] doSettermPropagation("
                      << x << ", " << S << std::endl;
 
-  Assert(S.getType().isSet() && S.getType().getSetElementType() == x.getType());
+  Assert(S.getType().isSet() && S.getType().getSetElementType() == x.getType(),
+         ( std::string("types of S and x are ") + S.getType().toString() +
+           std::string(" and ") + x.getType().toString() +
+           std::string(" respectively") ).c_str()  );
 
   Node literal, left_literal, right_literal;
 
@@ -416,7 +442,8 @@ const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements
         Unhandled();
       }
     } else {
-      Assert(k == kind::VARIABLE || k == kind::APPLY_UF);
+      Assert(k == kind::VARIABLE || k == kind::APPLY_UF || k == kind::SKOLEM,
+             (std::string("Expect variable or UF got ") + kindToString(k)).c_str() );
       /* assign emptyset, which is default */
     }
 
@@ -598,6 +625,7 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel)
   BOOST_FOREACH( TNode setterm, settermsModEq ) {
     Elements elements = getElements(setterm, settermElementsMap);
     Node shape = elementsToShape(elements, setterm.getType());
+    shape = theory::Rewriter::rewrite(shape);
     m->assertEquality(shape, setterm, true);
     m->assertRepresentative(shape);
   }
@@ -1042,6 +1070,14 @@ const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) {
   return d_info[x]->parents;
 }
 
+const CDTNodeList* TheorySetsPrivate::TermInfoManager::getMembers(TNode S) {
+  return d_info[S]->elementsInThisSet;
+}
+
+const CDTNodeList* TheorySetsPrivate::TermInfoManager::getNonMembers(TNode S) {
+  return d_info[S]->elementsNotInThisSet;
+}
+
 void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
   unsigned numChild = n.getNumChildren();
 
@@ -1052,8 +1088,7 @@ void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
 
   if(n.getKind() == kind::UNION ||
      n.getKind() == kind::INTERSECTION ||
-     n.getKind() == kind::SETMINUS ||
-     n.getKind() == kind::SET_SINGLETON) {
+     n.getKind() == kind::SETMINUS) {
 
     for(unsigned i = 0; i < numChild; ++i) {
       if(d_terms.contains(n[i])) {
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 7e9d60905..9225bfbfd 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -118,6 +118,8 @@ private:
     ~TermInfoManager();
     void notifyMembership(TNode fact);
     const CDTNodeList* getParents(TNode x);
+    const CDTNodeList* getMembers(TNode S);
+    const CDTNodeList* getNonMembers(TNode S);
     void addTerm(TNode n);
     void mergeTerms(TNode a, TNode b);
   };
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 328592abb..bcfbc46ae 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -201,12 +201,13 @@ const Elements& collectConstantElements(TNode setterm, SettermElementsMap& sette
         break;
       case kind::SET_SINGLETON:
         Assert(setterm[0].isConst());
-        cur.insert(setterm[0]);
+        cur.insert(TheorySetsRewriter::preRewrite(setterm[0]).node);
         break;
       default:
         Unhandled();
       }
     }
+    Debug("sets-rewrite-constant") << "[sets-rewrite-constant] "<< setterm << " " << setterm.getId() << std::endl;
 
     it = settermElementsMap.insert(SettermElementsMap::value_type(setterm, cur)).first;
   }
@@ -246,7 +247,10 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
     //rewrite set to normal form
     SettermElementsMap setTermElementsMap;   // cache
     const Elements& elements = collectConstantElements(node, setTermElementsMap);
-    return RewriteResponse(REWRITE_DONE, elementsToNormalConstant(elements, node.getType()));
+    RewriteResponse response(REWRITE_DONE, elementsToNormalConstant(elements, node.getType()));
+    Debug("sets-rewrite-constant") << "[sets-rewrite-constant] Rewriting " << node << std::endl
+                                   << "[sets-rewrite-constant]        to " << response.node << std::endl;
+    return response;
   }
 
   return RewriteResponse(REWRITE_DONE, node);
diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h
index 715817508..6ce418e85 100644
--- a/src/theory/sets/theory_sets_rewriter.h
+++ b/src/theory/sets/theory_sets_rewriter.h
@@ -83,7 +83,6 @@ public:
   static inline void shutdown() {
     // nothing to do
   }
-
 };/* class TheorySetsRewriter */
 
 }/* CVC4::theory::sets namespace */
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 203f116bb..6c0018c05 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -70,8 +70,8 @@ Node TheoryModel::getValue(TNode n) const {
     //normalize
     nn = Rewriter::rewrite(nn);
   }
-  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ):  returning"
-                          << nn << std::endl;
+  Debug("model-getvalue") << "[model-getvalue] getValue( " << n << " ): " << std::endl
+                          << "[model-getvalue] returning " << nn << std::endl;
   return nn;
 }
 
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 6d718553d..7f1f07461 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -31,6 +31,7 @@ TESTS =	\
 	jan24/remove_check_free_31_6.smt2 \
 	sets-inter.smt2 \
 	sets-equal.smt2 \
+	sets-disequal.smt2 \
 	union-2.smt2 \
 	jan27/deepmeas0.hs.fqout.cvc4.41.smt2 \
 	jan27/ListConcat.hs.fqout.cvc4.177.smt2 \
@@ -69,10 +70,10 @@ EXTRA_DIST = $(TESTS)
 #TESTS += \
 #	error.cvc
 #endif
-#
-# and make sure to distribute it
-#EXTRA_DIST += \
-#	error.cvc
+
+# disabled tests, yet distribute
+EXTRA_DIST += \
+	setofsets-disequal.smt2
 
 # synonyms for "check"
 .PHONY: regress regress0 test
diff --git a/test/regress/regress0/sets/setofsets-disequal.smt2 b/test/regress/regress0/sets/setofsets-disequal.smt2
new file mode 100644
index 000000000..907e074fe
--- /dev/null
+++ b/test/regress/regress0/sets/setofsets-disequal.smt2
@@ -0,0 +1,64 @@
+; On a production build (as of 2014-05-16), takes several minutes
+; to finish (2967466 decisions).
+
+(set-logic QF_BV_SETS)
+(set-info :status unsat)
+
+(define-sort myset () (Set (Set (_ BitVec 1))))
+(declare-fun S () myset)
+
+; 0 elements
+(assert (not (= S (as emptyset myset))))
+
+; 1 element is S
+(assert (not (= S (setenum (as emptyset (Set (_ BitVec 1)))))))
+(assert (not (= S (setenum (setenum (_ bv0 1)) ))))
+(assert (not (= S (setenum (setenum (_ bv1 1)) ))))
+(assert (not (= S (setenum (union (setenum (_ bv0 1))
+                                  (setenum (_ bv1 1)))))))
+
+; 2 elements in S
+(assert (not (= S (union (setenum (as emptyset (Set (_ BitVec 1))))
+                         (setenum (setenum (_ bv0 1)))) )))
+(assert (not (= S (union (setenum (as emptyset (Set (_ BitVec 1))))
+                         (setenum (setenum (_ bv1 1)))))))
+(assert (not (= S (union (setenum (as emptyset (Set (_ BitVec 1))))
+                         (setenum (union (setenum (_ bv0 1))
+                                         (setenum (_ bv1 1))))))))
+(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
+                                         (setenum (_ bv1 1))))
+                         (setenum (setenum (_ bv0 1)))) )))
+(assert (not (= S (union (setenum (setenum (_ bv0 1)))
+                         (setenum (setenum (_ bv1 1))))   )))
+(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
+                                         (setenum (_ bv1 1))))
+                         (setenum (setenum (_ bv1 1)))))))
+
+; 3 elements in S
+(assert (not (= S (union (setenum (setenum (_ bv1 1)))
+                         (union (setenum (as emptyset (Set (_ BitVec 1))))
+                                (setenum (setenum (_ bv0 1)))))  )))
+(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
+                                         (setenum (_ bv1 1))))
+                         (union (setenum (as emptyset (Set (_ BitVec 1))))
+                                (setenum (setenum (_ bv1 1)))))  )))
+(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
+                                         (setenum (_ bv1 1))))
+                         (union (setenum (setenum (_ bv0 1)))
+                                (setenum (setenum (_ bv1 1)))))  )))
+(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
+                                         (setenum (_ bv1 1))))
+                         (union (setenum (as emptyset (Set (_ BitVec 1))))
+                                (setenum (setenum (_ bv0 1)))))  )))
+
+; 4 elements in S
+(assert (not (= S (union (setenum (union (setenum (_ bv0 1))
+                                         (setenum (_ bv1 1))))
+                         (union (setenum (setenum (_ bv1 1)))
+                                (union (setenum (as emptyset (Set (_ BitVec 1))))
+                                       (setenum (setenum (_ bv0 1))))))  )))
+
+(check-sat)
+
+; if you delete any of the above assertions, you should get sat
+; (get-model)
diff --git a/test/regress/regress0/sets/sets-disequal.smt2 b/test/regress/regress0/sets/sets-disequal.smt2
new file mode 100644
index 000000000..65f55f3a6
--- /dev/null
+++ b/test/regress/regress0/sets/sets-disequal.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+; EXIT: 0
+(set-logic QF_BV_SETS)
+(declare-fun S1 () (Set (_ BitVec 1)))
+(declare-fun S2 () (Set (_ BitVec 1)))
+(declare-fun S3 () (Set (_ BitVec 1)))
+(declare-fun S4 () (Set (_ BitVec 1)))
+(assert (distinct S1 S2 S3 S4))
+(check-sat)
+;(get-model)
+(declare-fun S5 () (Set (_ BitVec 1)))
+(assert (not (= S5 S1)))
+(assert (not (= S5 S2)))
+(assert (not (= S5 S3)))
+(check-sat)
+(assert (not (= S5 S4)))
+(check-sat)