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 62f5ad3ffb4ec27487a679082c86c1cb3a1ec8a3..516aae0e14e6d05b72e760de428f1fdf72cf02a5 100644 (file)
--- 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 c375d68f22797744ff26594777fd2ea6e2bd3756..0e365c8754aef9362504cb7d546be732988dde04 100644 (file)
--- 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 22adf427dbadeeab8548b066fa96e96197c09d06..40364eeb77d9973e6ac2420f0449c1bede71fadb 100644 (file)
--- 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 eede5c3a83d0326a706f0c519d8bb63ac0f2cd80..6ec347031bcc8ac38ff8aec074a92b94f3ad1bd0 100644 (file)
--- 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 0b606ecf0363eaa0f68f1f41f2f7478bf7575017..3f6f2a6ed46c32c0d10566a13569a9a627b8bee3 100644 (file)
--- 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 dbd12f8f078f2611bb43b93e18abb424510209f7..e40635d4e7d90d2947850dd9ff3bf162f62988a5 100644 (file)
--- 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 06dc1fe58e0a5164fc07334c7f59407c66701944..68665f629566833cce4857b67512c86ec900220d 100644 (file)
--- 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 67f25bb72b32d34a41367808b4a606de5f5fc4e7..3d57288cf1dcdf6bcb05e6a8bfc24118be4a4218 100644 (file)
--- 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 "<")))