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

4 files changed, 53 insertions, 6 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index c497fcd0d..e6d7f9d86 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -931,7 +931,10 @@ toplevelDeclaration[CVC4::Command*& cmd]
  * A bound variable declaration.
  */
 boundVarDecl[std::vector<std::string>& ids, CVC4::Type& t]
-  : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON declareVariables[*(Command**)NULL,t,ids,false]
+@init {
+  Command* local_cmd = NULL;
+}
+  : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON declareVariables[local_cmd,t,ids,false]
   ;
 
 /**
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 38163c579..29d3e45b6 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -749,7 +749,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
       $cmd = new EmptyCommand();
     }
   | /* check-synth */
-    CHECK_SYNTH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    CHECK_SYNTH_TOK { PARSER_STATE->checkThatLogicIsSet();PARSER_STATE->defineSygusFuns(); }
     { Expr sygusVar = EXPR_MANAGER->mkVar("sygus", EXPR_MANAGER->booleanType());
       Expr sygusAttr = EXPR_MANAGER->mkExpr(kind::INST_PATTERN_LIST, EXPR_MANAGER->mkExpr(kind::INST_ATTRIBUTE, sygusVar));
       std::vector<Expr> bodyv;
@@ -760,7 +760,9 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
         body = EXPR_MANAGER->mkExpr(kind::EXISTS, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusVars()), body);
         Debug("parser-sygus") << "...constructed exists " << body << std::endl;   
       }
-      body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr);
+      if( !PARSER_STATE->getSygusFunSymbols().empty() ){
+        body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr);
+      }
       Debug("parser-sygus") << "...constructed forall " << body << std::endl;   
       Command* c = new SetUserAttributeCommand("sygus", sygusVar);
       c->setMuted(true);
@@ -791,6 +793,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
   std::string sname;
   std::vector< Expr > let_vars;
   bool readingLet = false;
+  std::string s;
 }
   : LPAREN_TOK
     //read operator
@@ -799,6 +802,8 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
         //since we enforce satisfaction completeness, immediately convert to total version
         if( k==CVC4::kind::BITVECTOR_UDIV ){
           k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
+        }else if( k==CVC4::kind::BITVECTOR_UREM ){
+          k = CVC4::kind::BITVECTOR_UREM_TOTAL;
         }
         sgt.d_name = kind::kindToString(k);
         sgt.d_gterm_type = SygusGTerm::gterm_op;
@@ -834,6 +839,8 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
           k = PARSER_STATE->getOperatorKind(name);
           if( k==CVC4::kind::BITVECTOR_UDIV ){
             k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
+          }else if( k==CVC4::kind::BITVECTOR_UREM ){
+            k = CVC4::kind::BITVECTOR_UREM_TOTAL;
           }
           sgt.d_name = kind::kindToString(k);
           sgt.d_gterm_type = SygusGTerm::gterm_op;
@@ -890,6 +897,12 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
       sgt.d_name = AntlrInput::tokenText($BINARY_LITERAL);
       sgt.d_gterm_type = SygusGTerm::gterm_op;
     }
+  | str[s,false]
+    { Debug("parser-sygus") << "Sygus grammar " << fun << " : string literal \"" << s << "\"" << std::endl;
+      sgt.d_expr = MK_CONST( ::CVC4::String(s) );
+      sgt.d_name = s;
+      sgt.d_gterm_type = SygusGTerm::gterm_op;
+    }
   | symbol[name,CHECK_NONE,SYM_VARIABLE] ( SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE] { readEnum = true; } )?
     { if( readEnum ){
         name = name + "__Enum__" + name2;
@@ -1594,6 +1607,10 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         Debug("parser") << "Empty set encountered: " << f << " "
                           << f2 << " " << type <<  std::endl;
         expr = MK_CONST( ::CVC4::EmptySet(type) );
+      } else if(f.getKind() == CVC4::kind::SEP_NIL_REF) {
+        //We don't want the nil reference to be a constant: for instance, it could be of type Int but is not a const rational.
+        //However, the expression has 0 children. So we convert to a SEP_NIL variable.
+        expr = EXPR_MANAGER->mkSepNil(type);
       } else {
         if(f.getType() != type) {
           PARSER_STATE->parseError("Type ascription not satisfied.");
@@ -1898,6 +1915,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   | EMPTYSET_TOK
     { expr = MK_CONST( ::CVC4::EmptySet(Type())); }
 
+  | NILREF_TOK
+    { expr = MK_CONST( ::CVC4::NilRef(Type())); }
     // NOTE: Theory constants go here
   ;
 
@@ -2633,6 +2652,7 @@ FMFCARDVAL_TOK : 'fmf.card.val';
 INST_CLOSURE_TOK : 'inst-closure';
 
 EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
+NILREF_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'sep.nil';
 // Other set theory operators are not
 // tokenized and handled directly when
 // processing a term
@@ -2773,7 +2793,7 @@ STRING_LITERAL_2_0
  * will be part of the token text.  Use the str[] parser rule instead.
  */
 STRING_LITERAL_2_5
-  : { PARSER_STATE->v2_5() }?=>
+  : { PARSER_STATE->v2_5() || PARSER_STATE->sygus() }?=>
     '"' (~('"') | '""')* '"'
   ;
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 463adcb54..9f3c43f09 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -166,6 +166,16 @@ void Smt2::addFloatingPointOperators() {
   Parser::addOperator(kind::FLOATINGPOINT_TO_SBV);
 }
 
+void Smt2::addSepOperators() {
+  addOperator(kind::SEP_STAR, "sep");
+  addOperator(kind::SEP_PTO, "pto");
+  addOperator(kind::SEP_WAND, "wand");
+  addOperator(kind::SEP_EMP, "emp");
+  Parser::addOperator(kind::SEP_STAR);
+  Parser::addOperator(kind::SEP_PTO);
+  Parser::addOperator(kind::SEP_WAND);
+  Parser::addOperator(kind::SEP_EMP);
+}
 
 void Smt2::addTheory(Theory theory) {
   switch(theory) {
@@ -258,7 +268,11 @@ void Smt2::addTheory(Theory theory) {
     defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
     addFloatingPointOperators();
     break;
-
+    
+  case THEORY_SEP:
+    addSepOperators();
+    break;
+    
   default:
     std::stringstream ss;
     ss << "internal error: unsupported theory " << theory;
@@ -311,6 +325,8 @@ bool Smt2::isTheoryEnabled(Theory theory) const {
     return d_logic.isTheoryEnabled(theory::THEORY_UF);
   case THEORY_FP:
     return d_logic.isTheoryEnabled(theory::THEORY_FP);
+  case THEORY_SEP:
+    return d_logic.isTheoryEnabled(theory::THEORY_SEP);
   default:
     std::stringstream ss;
     ss << "internal error: unsupported theory " << theory;
@@ -354,6 +370,8 @@ void Smt2::setLogic(std::string name) {
       name = "UFLIRA";
     } else if(name == "BV") {
       name = "UFBV";
+    } else if(name == "SLIA") {
+      name = "UFSLIA";
     } else if(name == "ALL_SUPPORTED") {
       //no change
     } else {
@@ -417,6 +435,10 @@ void Smt2::setLogic(std::string name) {
     addTheory(THEORY_FP);
   }
 
+  if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
+    addTheory(THEORY_SEP);
+  }
+  
 }/* Smt2::setLogic() */
 
 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 1ae2c9dd7..b99e142ba 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -51,7 +51,8 @@ public:
     THEORY_SETS,
     THEORY_STRINGS,
     THEORY_UF,
-    THEORY_FP
+    THEORY_FP,
+    THEORY_SEP
   };
 
 private:
@@ -344,6 +345,7 @@ private:
 
   void addFloatingPointOperators();
 
+  void addSepOperators();
 };/* class Smt2 */
 
 }/* CVC4::parser namespace */