summaryrefslogtreecommitdiff
path: root/src/parser/tptp
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/tptp')
-rw-r--r--src/parser/tptp/Tptp.g24
-rw-r--r--src/parser/tptp/tptp.cpp19
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);
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback