New C++ API: Keep reference to solver object in non-solver objects. (#4549)

This is in preparation for adding guards to ensure that sort and term
arguments belong to the same solver.

1 files changed, 30 insertions, 13 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 8e4152e2e..fdb6a081c 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,
-              t.getType(),
+              api::Sort(PARSER_STATE->getSolver(), t.getType()),
               ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
           PARSER_STATE->defineVar(*i, f);
           Command* decl =
@@ -1654,7 +1654,9 @@ tupleStore[CVC4::api::Term& f]
       }
       const Datatype & dt = ((DatatypeType)t.getType()).getDatatype();
       f2 = SOLVER->mkTerm(
-          api::APPLY_SELECTOR, api::Term(dt[0][k].getSelector()), f);
+          api::APPLY_SELECTOR,
+          api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()),
+          f);
     }
     ( ( arrayStore[f2]
       | DOT ( tupleStore[f2]
@@ -1687,7 +1689,9 @@ recordStore[CVC4::api::Term& f]
       }
       const Datatype & dt = ((DatatypeType)t.getType()).getDatatype();
       f2 = SOLVER->mkTerm(
-          api::APPLY_SELECTOR, api::Term(dt[0][id].getSelector()), f);
+          api::APPLY_SELECTOR,
+          api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()),
+          f);
     }
     ( ( arrayStore[f2]
       | DOT ( tupleStore[f2]
@@ -1831,7 +1835,10 @@ 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(dt[0][id].getSelector()), f);
+          f = SOLVER->mkTerm(
+              api::APPLY_SELECTOR,
+              api::Term(PARSER_STATE->getSolver(), dt[0][id].getSelector()),
+              f);
         }
       | k=numeral
         {
@@ -1846,7 +1853,10 @@ 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(dt[0][k].getSelector()), f);
+          f = SOLVER->mkTerm(
+              api::APPLY_SELECTOR,
+              api::Term(PARSER_STATE->getSolver(), dt[0][k].getSelector()),
+              f);
         }
       )
     )*
@@ -1857,7 +1867,7 @@ postfixTerm[CVC4::api::Term& f]
     | ABS_TOK LPAREN formula[f] RPAREN
       { f = MK_TERM(CVC4::api::ABS, f); }
     | DIVISIBLE_TOK LPAREN formula[f] COMMA n=numeral RPAREN
-      { f = MK_TERM(SOLVER->mkOp(CVC4::api::DIVISIBLE,n), f); }
+      { f = MK_TERM(SOLVER->mkOp(CVC4::api::DIVISIBLE, n), f); }
     | DISTINCT_TOK LPAREN
       formula[f] { args.push_back(f); }
       ( COMMA formula[f] { args.push_back(f); } )* RPAREN
@@ -1868,7 +1878,7 @@ postfixTerm[CVC4::api::Term& f]
     )
     ( typeAscription[f, t]
       {
-        f = PARSER_STATE->applyTypeAscription(f,t).getExpr();
+        f = PARSER_STATE->applyTypeAscription(f,t);
       }
     )?
   ;
@@ -1885,8 +1895,9 @@ relationTerm[CVC4::api::Term& f]
       args.push_back(f);
       types.push_back(f.getSort());
       api::Sort t = SOLVER->mkTupleSort(types);
-      const Datatype& dt = ((DatatypeType)t.getType()).getDatatype();
-      args.insert( args.begin(), api::Term(dt[0].getConstructor()) );
+      const Datatype& dt = Datatype(((DatatypeType)t.getType()).getDatatype());
+      args.insert(args.begin(),
+                  api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
       f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
     }
   | IDEN_TOK LPAREN formula[f] RPAREN
@@ -2136,7 +2147,9 @@ simpleTerm[CVC4::api::Term& f]
         }
         api::Sort dtype = SOLVER->mkTupleSort(types);
         const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
-        args.insert( args.begin(), dt[0].getConstructor() );
+        args.insert(
+            args.begin(),
+            api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
         f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
       }
     }
@@ -2146,7 +2159,9 @@ simpleTerm[CVC4::api::Term& f]
     { std::vector<api::Sort> types;
       api::Sort dtype = SOLVER->mkTupleSort(types);
       const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
-      f = MK_TERM(api::APPLY_CONSTRUCTOR, api::Term(dt[0].getConstructor())); }
+      f = MK_TERM(api::APPLY_CONSTRUCTOR,
+                  api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
+    }
 
     /* empty record literal */
   | PARENHASH HASHPAREN
@@ -2154,7 +2169,8 @@ simpleTerm[CVC4::api::Term& f]
       api::Sort dtype = SOLVER->mkRecordSort(
           std::vector<std::pair<std::string, api::Sort>>());
       const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
-      f = MK_TERM(api::APPLY_CONSTRUCTOR, api::Term(dt[0].getConstructor()));
+      f = MK_TERM(api::APPLY_CONSTRUCTOR,
+                  api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
     }
     /* empty set literal */
   | LBRACE RBRACE
@@ -2252,7 +2268,8 @@ simpleTerm[CVC4::api::Term& f]
       }
       api::Sort dtype = SOLVER->mkRecordSort(typeIds);
       const Datatype& dt = ((DatatypeType)dtype.getType()).getDatatype();
-      args.insert( args.begin(), dt[0].getConstructor() );
+      args.insert(args.begin(),
+                  api::Term(PARSER_STATE->getSolver(), dt[0].getConstructor()));
       f = MK_TERM(api::APPLY_CONSTRUCTOR, args);
     }