New C++ Api: First batch of API guards. (#4557)

This is the first batch of API guards, mainly extending existing guards
in the Solver object with checks that Ops, Terms, Sorts, and datatype objects
are associated to this solver object.

This further changes how DatatypeConstructorDecl objects are created. Previously,
they were not created via the Solver object (while DatatypeDecl was). Now, they are
created via Solver::mkDatatypeConstructorDecl, consistent with how DatatypeDecl
objects are created.

3 files changed, 23 insertions, 31 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index fdb6a081c..e604c7769 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1159,7 +1159,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t,
           PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE);
           api::Term func = PARSER_STATE->mkVar(
               *i,
-              api::Sort(PARSER_STATE->getSolver(), t.getType()),
+              api::Sort(SOLVER, t.getType()),
               ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
           PARSER_STATE->defineVar(*i, f);
           Command* decl =
@@ -1654,9 +1654,7 @@ tupleStore[CVC4::api::Term& f]
       }
       const Datatype & dt = ((DatatypeType)t.getType()).getDatatype();
       f2 = SOLVER->mkTerm(
-          api::APPLY_SELECTOR,
-          api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()),
-          f);
+          api::APPLY_SELECTOR, api::Term(SOLVER, dt[0][k].getSelector()), f);
     }
     ( ( arrayStore[f2]
       | DOT ( tupleStore[f2]
@@ -1689,9 +1687,7 @@ recordStore[CVC4::api::Term& f]
       }
       const Datatype & dt = ((DatatypeType)t.getType()).getDatatype();
       f2 = SOLVER->mkTerm(
-          api::APPLY_SELECTOR,
-          api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()),
-          f);
+          api::APPLY_SELECTOR, api::Term(SOLVER, dt[0][id].getSelector()), f);
     }
     ( ( arrayStore[f2]
       | DOT ( tupleStore[f2]
@@ -1835,10 +1831,9 @@ postfixTerm[CVC4::api::Term& f]
             PARSER_STATE->parseError(std::string("no such field `") + id + "' in record");
           }
           const Datatype & dt = ((DatatypeType)type.getType()).getDatatype();
-          f = SOLVER->mkTerm(
-              api::APPLY_SELECTOR,
-              api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()),
-              f);
+          f = SOLVER->mkTerm(api::APPLY_SELECTOR,
+                             api::Term(SOLVER, dt[0][id].getSelector()),
+                             f);
         }
       | k=numeral
         {
@@ -1853,10 +1848,9 @@ postfixTerm[CVC4::api::Term& f]
             PARSER_STATE->parseError(ss.str());
           }
           const Datatype & dt = ((DatatypeType)type.getType()).getDatatype();
-          f = SOLVER->mkTerm(
-              api::APPLY_SELECTOR,
-              api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()),
-              f);
+          f = SOLVER->mkTerm(api::APPLY_SELECTOR,
+                             api::Term(SOLVER, dt[0][k].getSelector()),
+                             f);
         }
       )
     )*
@@ -1896,8 +1890,7 @@ relationTerm[CVC4::api::Term& f]
       types.push_back(f.getSort());
       api::Sort t = SOLVER->mkTupleSort(types);
       const Datatype& dt = Datatype(((DatatypeType)t.getType()).getDatatype());
-      args.insert(args.begin(),
-                  api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+      args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor()));
       f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
     }
   | IDEN_TOK LPAREN formula[f] RPAREN
@@ -2147,9 +2140,7 @@ simpleTerm[CVC4::api::Term& f]
         }
         api::Sort dtype = SOLVER->mkTupleSort(types);
         const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
-        args.insert(
-            args.begin(),
-            api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+        args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor()));
         f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
       }
     }
@@ -2160,7 +2151,7 @@ simpleTerm[CVC4::api::Term& f]
       api::Sort dtype = SOLVER->mkTupleSort(types);
       const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
       f = MK_TERM(api::APPLY_CONSTRUCTOR,
-                  api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+                  api::Term(SOLVER, dt[0].getConstructor()));
     }
 
     /* empty record literal */
@@ -2170,7 +2161,7 @@ simpleTerm[CVC4::api::Term& f]
           std::vector<std::pair<std::string, api::Sort>>());
       const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
       f = MK_TERM(api::APPLY_CONSTRUCTOR,
-                  api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+                  api::Term(SOLVER, dt[0].getConstructor()));
     }
     /* empty set literal */
   | LBRACE RBRACE
@@ -2268,8 +2259,7 @@ simpleTerm[CVC4::api::Term& f]
       }
       api::Sort dtype = SOLVER->mkRecordSort(typeIds);
       const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
-      args.insert(args.begin(),
-                  api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+      args.insert(args.begin(), api::Term(SOLVER, dt[0].getConstructor()));
       f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
     }
 
@@ -2377,8 +2367,9 @@ constructorDef[CVC4::api::DatatypeDecl& type]
   std::unique_ptr<CVC4::api::DatatypeConstructorDecl> ctor;
 }
   : identifier[id,CHECK_UNDECLARED,SYM_SORT]
-    { 
-      ctor.reset(new CVC4::api::DatatypeConstructorDecl(id));
+    {
+      ctor.reset(new CVC4::api::DatatypeConstructorDecl(
+          SOLVER->mkDatatypeConstructorDecl(id)));
     }
     ( LPAREN
       selector[&ctor]
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f29e03380..62bf7e974 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -800,7 +800,7 @@ sygusGrammarV1[CVC4::api::Sort & ret,
 
     PARSER_STATE->getUnresolvedSorts().clear();
 
-    ret = api::Sort(PARSER_STATE->getSolver(), datatypeTypes[0]);
+    ret = api::Sort(SOLVER, datatypeTypes[0]);
   };
 
 // SyGuS grammar term.
@@ -1798,7 +1798,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
           if (Datatype::datatypeOf(ef).isParametric())
           {
             type = api::Sort(
-                PARSER_STATE->getSolver(),
+                SOLVER,
                 Datatype::datatypeOf(ef)[Datatype::indexOf(ef)]
                     .getSpecializedConstructorType(expr.getSort().getType()));
           }
@@ -2521,7 +2521,8 @@ constructorDef[CVC4::api::DatatypeDecl& type]
 }
   : symbol[id,CHECK_NONE,SYM_VARIABLE]
     {
-      ctor = new api::DatatypeConstructorDecl(id);
+      ctor = new api::DatatypeConstructorDecl(
+          SOLVER->mkDatatypeConstructorDecl(id));
     }
     ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
     { // make the constructor
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index c1d60ca31..e26709595 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -1441,7 +1441,7 @@ tffLetTermBinding[std::vector<CVC4::api::Term> & bvlist,
     PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false);
     std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
     rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
-    lhs = api::Term(PARSER_STATE->getSolver(), lhs.getExpr().getOperator());
+    lhs = api::Term(SOLVER, lhs.getExpr().getOperator());
   }
   | LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK
   ;
@@ -1463,7 +1463,7 @@ tffLetFormulaBinding[std::vector<CVC4::api::Term> & bvlist,
     PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true);
     std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
     rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
-    lhs = api::Term(PARSER_STATE->getSolver(), lhs.getExpr().getOperator());
+    lhs = api::Term(SOLVER, lhs.getExpr().getOperator());
   }
   | LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK
   ;