Merge branch 'interp' of https://git01.codeplex.com/z3 into interp

src/duality/duality.h

@@ -79,10 +79,6 @@ namespace Duality {
 
       int CumulativeDecisions();
 
-      Term SubstBoundRec(hash_map<int,hash_map<ast,Term> > &memo, hash_map<int,Term> &subst, int level, const Term &t);
-
-      Term SubstBound(hash_map<int,Term> &subst, const Term &t);
-
   private:
 
       void SummarizeRec(hash_set<ast> &memo, std::vector<expr> &lits, int &ops, const Term &t);
@@ -162,6 +158,12 @@ namespace Duality {
 				  bool weak = false
 				  ) = 0;
            
+	   /** Declare a constant in the background theory. */
+	   virtual void declare_constant(const func_decl &f) = 0;
+
+	   /** Is this a background constant? */
+	   virtual bool is_constant(const func_decl &f) = 0;
+
            /** Assert a background axiom. */
            virtual void assert_axiom(const expr &axiom) = 0;
 
@@ -224,10 +226,24 @@ namespace Duality {
 	  islvr->write_interpolation_problem(file_name,assumptions,theory);
 #endif
 	}
+
+	/** Declare a constant in the background theory. */
+	virtual void declare_constant(const func_decl &f){
+	  bckg.insert(f);
+	}
+	
+	/** Is this a background constant? */
+	virtual bool is_constant(const func_decl &f){
+	  return bckg.find(f) != bckg.end();
+	}
+
         ~iZ3LogicSolver(){
           // delete ictx;
           delete islvr;
         }
+      private:
+	hash_set<func_decl> bckg;
+
       };
 
 #if 0
@@ -478,6 +494,10 @@ namespace Duality {
       
       void AssertNode(Node *n);
 
+      /** Declare a constant in the background theory. */
+
+      void DeclareConstant(const FuncDecl &f);
+
       /** Assert a background axiom. Background axioms can be used to provide the
        *  theory of auxilliary functions or relations. All symbols appearing in
        *  background axioms are considered global, and may appear in both transformer
@@ -771,6 +791,12 @@ namespace Duality {
 
       void GetLabelsRec(hash_map<ast,int> &memo, const Term &f, std::vector<symbol> &labels,
 			hash_set<ast> *done, bool truth);
+
+      Term SubstBoundRec(hash_map<int,hash_map<ast,Term> > &memo, hash_map<int,Term> &subst, int level, const Term &t);
+
+      Term SubstBound(hash_map<int,Term> &subst, const Term &t);
+
+
     };
     
     /** RPFP solver base class. */

src/duality/duality_rpfp.cpp

@@ -205,7 +205,7 @@ namespace Duality {
 	if(rit != e->relMap.end())
 	  res = RedDualRela(e,args,(rit->second));
 	else {
-	  if (args.size() == 0 && f.get_decl_kind() == Uninterpreted)
+	  if (args.size() == 0 && f.get_decl_kind() == Uninterpreted && !ls->is_constant(f))
 	    {
 	      res = HideVariable(t,e->number);
 	    }
@@ -520,6 +520,12 @@ namespace Duality {
       }
   }
 
+  /** Declare a constant in the background theory. */
+
+  void RPFP::DeclareConstant(const FuncDecl &f){
+    ls->declare_constant(f);
+  }
+
   /** Assert a background axiom. Background axioms can be used to provide the
    *  theory of auxilliary functions or relations. All symbols appearing in
    *  background axioms are considered global, and may appear in both transformer
@@ -1828,7 +1834,7 @@ namespace Duality {
     return RemoveLabelsRec(memo,t,lbls);
   }
 
-  Z3User::Term Z3User::SubstBoundRec(hash_map<int,hash_map<ast,Term> > &memo, hash_map<int,Term> &subst, int level, const Term &t)
+  RPFP::Term RPFP::SubstBoundRec(hash_map<int,hash_map<ast,Term> > &memo, hash_map<int,Term> &subst, int level, const Term &t)
   {
     std::pair<ast,Term> foo(t,expr(ctx));
     std::pair<hash_map<ast,Term>::iterator, bool> bar = memo[level].insert(foo);
@@ -1839,6 +1845,8 @@ namespace Duality {
 	func_decl f = t.decl();
 	std::vector<Term> args;
 	int nargs = t.num_args();
+	if(nargs == 0)
+	  ls->declare_constant(f);  // keep track of background constants
 	for(int i = 0; i < nargs; i++)
 	  args.push_back(SubstBoundRec(memo, subst, level, t.arg(i)));
 	res = f(args.size(),&args[0]);
@@ -1858,7 +1866,7 @@ namespace Duality {
     return res;
   }
 
-  Z3User::Term Z3User::SubstBound(hash_map<int,Term> &subst, const Term &t){
+  RPFP::Term RPFP::SubstBound(hash_map<int,Term> &subst, const Term &t){
     hash_map<int,hash_map<ast,Term> > memo;
     return SubstBoundRec(memo, subst, 0, t);
   }
@@ -2037,7 +2045,7 @@ namespace Duality {
 	int nargs = t.num_args();
 	for(int i = 0; i < nargs; i++)
 	  WriteEdgeVars(e, memo, t.arg(i),s);
-	if (nargs == 0 && f.get_decl_kind() == Uninterpreted){
+	if (nargs == 0 && f.get_decl_kind() == Uninterpreted && !ls->is_constant(f)){
 	  Term rename = HideVariable(t,e->number);
 	  Term value = dualModel.eval(rename);
 	  s << " (= " << t << " " << value << ")\n";