Merge branch 'master' of https://github.com/CVC4/CVC4.git

Conflicts:
	proofs/signatures/Makefile.am
	src/Makefile.am
	src/expr/datatype.cpp
	src/options/datatypes_options
	src/options/options_template.cpp
	src/options/quantifiers_options
	src/proof/arith_proof.cpp
	src/proof/arith_proof.h
	src/proof/array_proof.cpp
	src/proof/array_proof.h
	src/proof/bitvector_proof.cpp
	src/proof/bitvector_proof.h
	src/proof/cnf_proof.cpp
	src/proof/cnf_proof.h
	src/proof/proof_manager.cpp
	src/proof/proof_manager.h
	src/proof/sat_proof.h
	src/proof/sat_proof_implementation.h
	src/proof/skolemization_manager.h
	src/proof/theory_proof.cpp
	src/proof/theory_proof.h
	src/proof/uf_proof.cpp
	src/proof/uf_proof.h
	src/prop/cnf_stream.cpp
	src/prop/cnf_stream.h
	src/prop/minisat/core/Solver.cc
	src/prop/prop_engine.cpp
	src/prop/prop_engine.h
	src/prop/theory_proxy.cpp
	src/smt/smt_engine.cpp
	src/smt/smt_engine_check_proof.cpp
	src/theory/arrays/array_proof_reconstruction.cpp
	src/theory/arrays/theory_arrays.cpp
	src/theory/bv/eager_bitblaster.cpp
	src/theory/bv/lazy_bitblaster.cpp
	src/theory/datatypes/theory_datatypes.cpp
	src/theory/quantifiers/alpha_equivalence.cpp
	src/theory/quantifiers/candidate_generator.cpp
	src/theory/quantifiers/candidate_generator.h
	src/theory/quantifiers/ce_guided_single_inv.cpp
	src/theory/quantifiers/ceg_instantiator.cpp
	src/theory/quantifiers/conjecture_generator.cpp
	src/theory/quantifiers/equality_infer.cpp
	src/theory/quantifiers/equality_infer.h
	src/theory/quantifiers/inst_match_generator.cpp
	src/theory/quantifiers/inst_propagator.cpp
	src/theory/quantifiers/inst_propagator.h
	src/theory/quantifiers/inst_strategy_e_matching.cpp
	src/theory/quantifiers/inst_strategy_e_matching.h
	src/theory/quantifiers/instantiation_engine.cpp
	src/theory/quantifiers/model_builder.cpp
	src/theory/quantifiers/model_engine.cpp
	src/theory/quantifiers/quant_conflict_find.cpp
	src/theory/quantifiers/quant_conflict_find.h
	src/theory/quantifiers/quant_split.cpp
	src/theory/quantifiers/quant_util.cpp
	src/theory/quantifiers/quantifiers_rewriter.cpp
	src/theory/quantifiers/quantifiers_rewriter.h
	src/theory/quantifiers/term_database.cpp
	src/theory/quantifiers/term_database.h
	src/theory/quantifiers/trigger.cpp
	src/theory/quantifiers/trigger.h
	src/theory/quantifiers_engine.cpp
	src/theory/quantifiers_engine.h
	src/theory/sets/kinds
	src/theory/sets/theory_sets_private.cpp
	src/theory/sets/theory_sets_private.h
	src/theory/sets/theory_sets_rewriter.cpp
	src/theory/sets/theory_sets_type_rules.h
	src/theory/strings/theory_strings.cpp
	src/theory/strings/theory_strings.h
	src/theory/theory_engine.cpp
	src/theory/theory_engine.h
	src/theory/uf/equality_engine.cpp
	test/regress/regress0/fmf/Makefile.am
	test/regress/regress0/quantifiers/Makefile.am
	test/regress/regress0/strings/Makefile.am
	test/regress/regress0/sygus/Makefile.am
	test/regress/regress0/sygus/max2-univ.sy

11 files changed, 174 insertions, 17 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index c04de4421..9dcbc3b4b 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -40,6 +40,8 @@ libexpr_la_SOURCES = \
 	pickle_data.h \
 	pickler.cpp \
 	pickler.h \
+	sepconst.cpp \
+	sepconst.h \
 	symbol_table.cpp \
 	symbol_table.h \
 	type.cpp \
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index d14ac26d4..12cab48cc 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -297,7 +297,7 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) {
   return true;
 }
 
-bool Datatype::isUFinite() const throw(IllegalArgumentException) {
+bool Datatype::isInterpretedFinite() const throw(IllegalArgumentException) {
   PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_self);
@@ -310,7 +310,7 @@ bool Datatype::isUFinite() const throw(IllegalArgumentException) {
   self.setAttribute(DatatypeUFiniteComputedAttr(), true);
   self.setAttribute(DatatypeUFiniteAttr(), false);
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    if(! (*i).isUFinite()) {
+    if(! (*i).isInterpretedFinite()) {
       return false;
     }
   }
@@ -850,7 +850,7 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
   return true;
 }
 
-bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) {
+bool DatatypeConstructor::isInterpretedFinite() const throw(IllegalArgumentException) {
   PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
   // we're using some internals, so we have to set up this library context
   ExprManagerScope ems(d_constructor);
@@ -861,16 +861,8 @@ bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) {
   }
   bool success = true;
   for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
-    Type t = (*i).getRangeType();
-    if( t.isDatatype() ){
-      const Datatype& dt = ((DatatypeType)t).getDatatype();
-      if( !dt.isUFinite() ){
-        success = false;
-      }
-    }else if(!t.isSort() && !t.getCardinality().isFinite()) {
-      success = false;
-    }
-    if(!success ){
+    TypeNode t = TypeNode::fromType( (*i).getRangeType() );
+    if(!t.isInterpretedFinite()) {
       self.setAttribute(DatatypeUFiniteComputedAttr(), true);
       self.setAttribute(DatatypeUFiniteAttr(), false);
       return false;
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 1197b4a3b..a0c9cbe6b 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -342,7 +342,7 @@ public:
    * uninterpreted sorts are finite.  This function can
    * only be called for resolved constructors.
    */
-  bool isUFinite() const throw(IllegalArgumentException);
+  bool isInterpretedFinite() const throw(IllegalArgumentException);
 
   /**
    * Returns true iff this Datatype constructor has already been
@@ -613,6 +613,9 @@ public:
   /** get the record representation for this datatype */
   inline Record * getRecord() const;
 
+  /** get the record representation for this datatype */
+  inline Record * getRecord() const;
+
   /**
    * Return the cardinality of this datatype (the sum of the
    * cardinalities of its constructors).  The Datatype must be
@@ -634,7 +637,7 @@ public:
    * datatype is  not well-founded, this function  returns false.  The
    * Datatype must be resolved or an exception is thrown.
    */
-  bool isUFinite() const throw(IllegalArgumentException);
+  bool isInterpretedFinite() const throw(IllegalArgumentException);
 
   /**
    * Return true iff this datatype is well-founded (there exist ground
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 84f674d2b..53e16751e 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -30,7 +30,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 33 "${template}"
+#line 34 "${template}"
 
 #ifdef CVC4_STATISTICS_ON
   #define INC_STAT(kind) \
@@ -941,6 +941,11 @@ Expr ExprManager::mkBoundVar(Type type) {
   return Expr(this, d_nodeManager->mkBoundVarPtr(*type.d_typeNode));
 }
 
+Expr ExprManager::mkSepNil(Type type) {
+  NodeManagerScope nms(d_nodeManager);
+  return Expr(this, d_nodeManager->mkSepNilPtr(*type.d_typeNode));
+}
+
 Expr ExprManager::mkAssociative(Kind kind,
                                 const std::vector<Expr>& children) {
   PrettyCheckArgument(
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 04f2f4289..9c4e554e1 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -124,6 +124,9 @@ public:
   /** Get the type for regular expressions. */
   RegExpType regExpType() const;
 
+  /** Get the type for regular expressions. */
+  RegExpType regExpType() const;
+
   /** Get the type for reals. */
   RealType realType() const;
 
@@ -545,6 +548,11 @@ public:
    * @param type the type for the new bound variable
    */
   Expr mkBoundVar(Type type);
+  
+  /**
+   * Create a (nameless) new nil reference for separation logic of type
+   */
+  Expr mkSepNil(Type type);
 
   /** Get a reference to the statistics registry for this ExprManager */
   Statistics getStatistics() const throw();
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 0809a0331..d2ac7e2a1 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -681,6 +681,20 @@ Node NodeManager::mkInstConstant(const TypeNode& type) {
   return n;
 }
 
+Node NodeManager::mkSepNil(const TypeNode& type) {
+  Node n = NodeBuilder<0>(this, kind::SEP_NIL);
+  n.setAttribute(TypeAttr(), type);
+  n.setAttribute(TypeCheckedAttr(), true);
+  return n;
+}
+
+Node* NodeManager::mkSepNilPtr(const TypeNode& type) {
+  Node* n = NodeBuilder<0>(this, kind::SEP_NIL).constructNodePtr();
+  setAttribute(*n, TypeAttr(), type);
+  setAttribute(*n, TypeCheckedAttr(), true);
+  return n;
+}
+
 Node NodeManager::mkAbstractValue(const TypeNode& type) {
   Node n = mkConst(AbstractValue(++d_abstractValueCount));
   n.setAttribute(TypeAttr(), type);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 7d2b13e4c..dcd7005f8 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -332,7 +332,7 @@ class NodeManager {
   /** Create a variable with the given type. */
   Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
   Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
-
+  
 public:
 
   explicit NodeManager(ExprManager* exprManager);
@@ -486,6 +486,10 @@ public:
 
   /** Create a instantiation constant with the given type. */
   Node mkInstConstant(const TypeNode& type);
+  
+  /** Create nil reference for separation logic with the given type. */
+  Node mkSepNil(const TypeNode& type);
+  Node* mkSepNilPtr(const TypeNode& type);
 
   /** Make a new abstract value with the given type. */
   Node mkAbstractValue(const TypeNode& type);
diff --git a/src/expr/sepconst.cpp b/src/expr/sepconst.cpp
new file mode 100644
index 000000000..7646b90d3
--- /dev/null
+++ b/src/expr/sepconst.cpp
@@ -0,0 +1,29 @@
+/*********************                                                        */
+/*! \file sepconst.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** 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 "expr/sepconst.h"
+#include <iostream>
+
+using namespace std;
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const NilRef& asa) {
+  return out << "(nil " << asa.getType() << ")";
+}
+
+}/* CVC4 namespace */
diff --git a/src/expr/sepconst.h b/src/expr/sepconst.h
new file mode 100644
index 000000000..9f86c7efc
--- /dev/null
+++ b/src/expr/sepconst.h
@@ -0,0 +1,72 @@
+/*********************                                                        */
+/*! \file sepconst.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** 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 "cvc4_public.h"
+
+#pragma once
+
+namespace CVC4 {
+  // messy; Expr needs NilRef (because it's the payload of a
+  // CONSTANT-kinded expression), and NilRef needs Expr.
+  class CVC4_PUBLIC NilRef;
+  //class CVC4_PUBLIC EmpStar;
+}/* CVC4 namespace */
+
+#include "expr/expr.h"
+#include "expr/type.h"
+#include <iostream>
+
+namespace CVC4 {
+
+class CVC4_PUBLIC NilRef {
+  const Type d_type;
+  NilRef() { }
+public:
+  NilRef(Type refType):d_type(refType) { }
+
+  ~NilRef() throw() {
+  }
+  Type getType() const { return d_type; }
+  bool operator==(const NilRef& es) const throw() {
+    return d_type == es.d_type;
+  }
+  bool operator!=(const NilRef& es) const throw() {
+    return !(*this == es);
+  }
+  bool operator<(const NilRef& es) const throw() {
+    return d_type < es.d_type;
+  }
+  bool operator<=(const NilRef& es) const throw() {
+    return d_type <= es.d_type;
+  }
+  bool operator>(const NilRef& es) const throw() {
+    return !(*this <= es);
+  }
+  bool operator>=(const NilRef& es) const throw() {
+    return !(*this < es);
+  }
+};/* class NilRef */
+
+std::ostream& operator<<(std::ostream& out, const NilRef& es) CVC4_PUBLIC;
+
+struct CVC4_PUBLIC NilRefHashFunction {
+  inline size_t operator()(const NilRef& es) const {
+    return TypeHashFunction()(es.getType());
+  }
+};/* struct NilRefHashFunction */
+
+}/* CVC4 namespace */
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 5d672e6ac..dc2370bea 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -21,6 +21,7 @@
 #include "expr/type_properties.h"
 #include "options/base_options.h"
 #include "options/expr_options.h"
+#include "options/quantifiers_options.h"
 
 using namespace std;
 
@@ -64,6 +65,26 @@ Cardinality TypeNode::getCardinality() const {
   return kind::getCardinality(*this);
 }
 
+bool TypeNode::isInterpretedFinite() const {
+  if( getCardinality().isFinite() ){
+    return true;
+  }else{
+    if( options::finiteModelFind() ){
+      if( isSort() ){
+        return true;
+      }else if( isDatatype() || isParametricDatatype() ){
+        const Datatype& dt = getDatatype();
+        return dt.isInterpretedFinite();
+      }else if( isArray() ){
+        return getArrayIndexType().isInterpretedFinite() && getArrayConstituentType().isInterpretedFinite();
+      }else if( isSet() ) {
+        return getSetElementType().isInterpretedFinite();
+      }
+    }
+    return false;
+  }
+}
+
 bool TypeNode::isWellFounded() const {
   return kind::isWellFounded(*this);
 }
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index cfb61a085..46fdaa143 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -419,6 +419,13 @@ public:
    * @return a finite or infinite cardinality
    */
   Cardinality getCardinality() const;
+  
+  /**
+   * Is this type interpreted as being finite.
+   * If finite model finding is enabled, this assumes all uninterpreted sorts 
+   *   are interpreted as finite.
+   */
+  bool isInterpretedFinite() const;
 
   /**
    * Returns whether this type is well-founded.