diff options
Diffstat (limited to 'src/parser/tptp')
-rw-r--r-- | src/parser/tptp/Tptp.g | 24 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 19 |
2 files changed, 18 insertions, 25 deletions
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 050a23320..b99376685 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -161,10 +161,10 @@ parseCommand returns [CVC4::Command* cmd = NULL] } (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK { - CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr); + CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr, expr); if( !aexpr.isNull() ){ // set the expression name (e.g. used with unsat core printing) - Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name); + Command* csen = new SetExpressionNameCommand(aexpr, name); csen->setMuted(true); PARSER_STATE->preemptCommand(csen); } @@ -178,7 +178,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr); if( !aexpr.isNull() ){ // set the expression name (e.g. used with unsat core printing) - Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name); + Command* csen = new SetExpressionNameCommand(aexpr, name); csen->setMuted(true); PARSER_STATE->preemptCommand(csen); } @@ -194,7 +194,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr); if( !aexpr.isNull() ){ // set the expression name (e.g. used with unsat core printing) - Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name); + Command* csen = new SetExpressionNameCommand(aexpr, name); csen->setMuted(true); PARSER_STATE->preemptCommand(csen); } @@ -219,7 +219,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] if (!aexpr.isNull()) { // set the expression name (e.g. used with unsat core printing) - Command* csen = new SetExpressionNameCommand(aexpr.getExpr(), name); + Command* csen = new SetExpressionNameCommand(aexpr, name); csen->setMuted(true); PARSER_STATE->preemptCommand(csen); } @@ -255,7 +255,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] CVC4::api::Term aexpr = PARSER_STATE->getAssertionDistinctConstants(); if( !aexpr.isNull() ) { - seq->addCommand(new AssertCommand(aexpr.getExpr(), false)); + seq->addCommand(new AssertCommand(aexpr, false)); } std::string filename = PARSER_STATE->getInput()->getInputStreamName(); @@ -268,7 +268,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] } seq->addCommand(new SetInfoCommand("filename", SExpr(filename))); if(PARSER_STATE->hasConjecture()) { - seq->addCommand(new QueryCommand(SOLVER->mkFalse().getExpr())); + seq->addCommand(new QueryCommand(SOLVER->mkFalse())); } else { seq->addCommand(new CheckSatCommand()); } @@ -967,7 +967,7 @@ thfAtomTyping[CVC4::Command*& cmd] { // as yet, it's undeclared api::Sort atype = PARSER_STATE->mkSort(name); - cmd = new DeclareTypeCommand(name, 0, atype.getType()); + cmd = new DeclareSortCommand(name, 0, atype); } } | parseThfType[type] @@ -1007,8 +1007,7 @@ thfAtomTyping[CVC4::Command*& cmd] { freshExpr = PARSER_STATE->bindVar(name, type); } - cmd = new DeclareFunctionCommand( - name, freshExpr.getExpr(), type.getType()); + cmd = new DeclareFunctionCommand(name, freshExpr, type); } } ) @@ -1320,7 +1319,7 @@ tffTypedAtom[CVC4::Command*& cmd] } else { // as yet, it's undeclared api::Sort atype = PARSER_STATE->mkSort(name); - cmd = new DeclareTypeCommand(name, 0, atype.getType()); + cmd = new DeclareSortCommand(name, 0, atype); } } | parseType[type] @@ -1339,8 +1338,7 @@ tffTypedAtom[CVC4::Command*& cmd] } else { // as yet, it's undeclared CVC4::api::Term aexpr = PARSER_STATE->bindVar(name, type); - cmd = - new DeclareFunctionCommand(name, aexpr.getExpr(), type.getType()); + cmd = new DeclareFunctionCommand(name, aexpr, type); } } ) diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 8f75cf8d3..066970fe3 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -76,8 +76,7 @@ void Tptp::addTheory(Theory theory) { { std::string d_unsorted_name = "$$unsorted"; d_unsorted = d_solver->mkUninterpretedSort(d_unsorted_name); - preemptCommand( - new DeclareTypeCommand(d_unsorted_name, 0, d_unsorted.getType())); + preemptCommand(new DeclareSortCommand(d_unsorted_name, 0, d_unsorted)); } // propositionnal defineType("Bool", d_solver->getBooleanSort()); @@ -243,8 +242,7 @@ api::Term Tptp::parseOpToExpr(ParseOp& p) api::Sort t = p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted; expr = bindVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero - preemptCommand( - new DeclareFunctionCommand(p.d_name, expr.getExpr(), t.getType())); + preemptCommand(new DeclareFunctionCommand(p.d_name, expr, t)); } return expr; } @@ -288,8 +286,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args) p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted; t = d_solver->mkFunctionSort(sorts, t); v = bindVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero - preemptCommand( - new DeclareFunctionCommand(p.d_name, v.getExpr(), t.getType())); + preemptCommand(new DeclareFunctionCommand(p.d_name, v, t)); } // args might be rationals, in which case we need to create // distinct constants of the "unsorted" sort to represent them @@ -394,13 +391,11 @@ api::Term Tptp::convertRatToUnsorted(api::Term expr) // Conversion from rational to unsorted t = d_solver->mkFunctionSort(d_solver->getRealSort(), d_unsorted); d_rtu_op = d_solver->mkConst(t, "$$rtu"); - preemptCommand( - new DeclareFunctionCommand("$$rtu", d_rtu_op.getExpr(), t.getType())); + preemptCommand(new DeclareFunctionCommand("$$rtu", d_rtu_op, t)); // Conversion from unsorted to rational t = d_solver->mkFunctionSort(d_unsorted, d_solver->getRealSort()); d_utr_op = d_solver->mkConst(t, "$$utr"); - preemptCommand( - new DeclareFunctionCommand("$$utr", d_utr_op.getExpr(), t.getType())); + preemptCommand(new DeclareFunctionCommand("$$utr", d_utr_op, t)); } // Add the inverse in order to show that over the elements that // appear in the problem there is a bijection between unsorted and @@ -410,7 +405,7 @@ api::Term Tptp::convertRatToUnsorted(api::Term expr) d_r_converted.insert(expr); api::Term eq = d_solver->mkTerm( api::EQUAL, expr, d_solver->mkTerm(api::APPLY_UF, d_utr_op, ret)); - preemptCommand(new AssertCommand(eq.getExpr())); + preemptCommand(new AssertCommand(eq)); } return api::Term(ret); } @@ -506,7 +501,7 @@ Command* Tptp::makeAssertCommand(FormulaRole fr, if( expr.isNull() ){ return new EmptyCommand("Untreated role for expression"); }else{ - return new AssertCommand(expr.getExpr(), inUnsatCore); + return new AssertCommand(expr, inUnsatCore); } } |