From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 31 Oct 2014 10:35:11 +0000 (+0100)
Subject: Do not allow duplication of function definitions.  Set incomplete flag in model builder.
X-Git-Tag: cvc5-1.0.0~6534
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=458b2b7eb5bdf09a1a886f4e2a165380d5fd918f;p=cvc5.git

Do not allow duplication of function definitions.  Set incomplete flag in model builder.
---

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 62f5ad3ff..516aae0e1 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1142,7 +1142,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
     }
   }
   Assert( !eq_merged );
-  */
+  //*/
 
   //combine the equality engine
   m->assertEqualityEngine( &d_equalityEngine );
@@ -1158,7 +1158,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
     }
   }
   Assert( !eq_merged );
-  */
+  //*/
 
   //get all constructors
   eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine );
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index c375d68f2..0e365c875 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -39,6 +39,12 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) {
         Assert( n.getKind()==APPLY_UF );
         Node f = n.getOperator();
         
+        //check if already defined, if so, throw error
+        if( d_sorts.find( f )!=d_sorts.end() ){
+          Message() << "Cannot define function " << f << " more than once." << std::endl;
+          exit( 0 );
+        }
+        
         //create a sort S that represents the inputs of the function
         std::stringstream ss;
         ss << "I_" << f;
diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h
index 22adf427d..40364eeb7 100644
--- a/src/theory/quantifiers/fun_def_process.h
+++ b/src/theory/quantifiers/fun_def_process.h
@@ -35,8 +35,6 @@ private:
   std::map< Node, TypeNode > d_sorts;
   //defined functions to injections input -> argument elements
   std::map< Node, std::vector< Node > > d_input_arg_inj;
-  //flatten ITE
-  void flattenITE( Node lhs, Node n, std::vector< std::vector< Node > >& conds, std::vector< Node >& terms );
   //simplify
   Node simplify( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, bool is_fun_def = false );
   //simplify term
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index eede5c3a8..6ec347031 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -96,6 +96,10 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
       //CVC4 will answer SAT or unknown
       Trace("fmf-consistent") << std::endl;
       debugPrint("fmf-consistent");
+      //if the check was incomplete, we must set incomplete flag
+      if( d_incomplete_check ){
+        d_quantEngine->getOutputChannel().setIncomplete();
+      }
     }else{
       //otherwise, the search will continue
     }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 0b606ecf0..3f6f2a6ed 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1031,6 +1031,14 @@ void TermDb::computeAttributes( Node q ) {
         if( avar.getAttribute(FunDefAttribute()) ){
           Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
           d_qattr_fundef[q] = true;
+          Assert( q[1].getKind()==EQUAL || q[1].getKind()==IFF );
+          Assert( q[1][0].getKind()==APPLY_UF );
+          Node f = q[1][0].getOperator();
+          if( d_fun_defs.find( f )!=d_fun_defs.end() ){
+            Message() << "Cannot define function " << f << " more than once." << std::endl;
+            exit( 0 );
+          }
+          d_fun_defs[f] = true;
         }
         if( avar.getAttribute(SygusAttribute()) ){
           //should be nested existential
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index dbd12f8f0..e40635d4e 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -310,7 +310,8 @@ public:
   /** filter all nodes that have instances */
   void filterInstances( std::vector< Node >& nodes );
 
-  
+private:
+  std::map< Node, bool > d_fun_defs;
 public: //general queries concerning quantified formulas wrt modules
   /** is quantifier treated as a rewrite rule? */
   static bool isRewriteRule( Node q );
diff --git a/test/regress/regress0/bug590.smt2 b/test/regress/regress0/bug590.smt2
index 06dc1fe58..68665f629 100644
--- a/test/regress/regress0/bug590.smt2
+++ b/test/regress/regress0/bug590.smt2
@@ -2,7 +2,7 @@
 (set-option :strings-exp true)
 (set-option :produce-models true)
 (set-info :smt-lib-version 2.0)
-(set-info :status sat)
+(set-info :status unknown)
 
 (declare-fun text () String)
 (declare-fun output () String)
diff --git a/test/regress/regress0/bug590.smt2.expect b/test/regress/regress0/bug590.smt2.expect
index 67f25bb72..3d57288cf 100644
--- a/test/regress/regress0/bug590.smt2.expect
+++ b/test/regress/regress0/bug590.smt2.expect
@@ -1,2 +1,2 @@
-% EXPECT: sat
+% EXPECT: unknown
 % EXPECT: ((charlst2 (store ((as const (Array Int String)) "C") 0 "&lt;")))