diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-07-24 10:11:24 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-24 10:11:24 -0700 |
commit | f270410e420d4c464c94c249e107451c5f1341ee (patch) | |
tree | 8abd41610443ec33efd6d41b0157cae5a490c6f0 /src/api | |
parent | c9f50eed48fa920320f93921415885f0042b9d39 (diff) |
New C++ API: First batch of commands (SMT-LIB and non-SMT-LIB). (#2199)
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cvc4cpp.cpp | 90 |
1 files changed, 90 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 53b87f2fa..dbaac4f8c 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2248,6 +2248,96 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) return res; } +/* Non-SMT-LIB commands */ +/* -------------------------------------------------------------------------- */ + +Term Solver::simplify(const Term& t) +{ + return d_smtEngine->simplify(*t.d_expr); +} + +Result Solver::checkValid(void) const +{ + // CHECK: + // if d_queryMade -> incremental enabled + CVC4::Result r = d_smtEngine->query(); + return Result(r); +} + +Result Solver::checkValidAssuming(Term assumption) const +{ + // CHECK: + // if assumptions.size() > 0: incremental enabled? + CVC4::Result r = d_smtEngine->query(*assumption.d_expr); + return Result(r); +} + +Result Solver::checkValidAssuming(const std::vector<Term>& assumptions) const +{ + // CHECK: + // if assumptions.size() > 0: incremental enabled? + std::vector<Expr> eassumptions = termVectorToExprs(assumptions); + CVC4::Result r = d_smtEngine->query(eassumptions); + return Result(r); +} + +/* SMT-LIB commands */ +/* -------------------------------------------------------------------------- */ + +/** + * ( assert <term> ) + */ +void Solver::assertFormula(Term term) const +{ + // CHECK: + // NodeManager::fromExprManager(d_exprMgr) + // == NodeManager::fromExprManager(expr.getExprManager()) + d_smtEngine->assertFormula(*term.d_expr); +} + +/** + * ( check-sat ) + */ +Result Solver::checkSat(void) const +{ + // CHECK: + // if d_queryMade -> incremental enabled + CVC4::Result r = d_smtEngine->checkSat(); + return Result(r); +} + +/** + * ( check-sat-assuming ( <prop_literal> ) ) + */ +Result Solver::checkSatAssuming(Term assumption) const +{ + // CHECK: + // if assumptions.size() > 0: incremental enabled? + CVC4::Result r = d_smtEngine->checkSat(*assumption.d_expr); + return Result(r); +} + +/** + * ( check-sat-assuming ( <prop_literal>* ) ) + */ +Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const +{ + // CHECK: + // if assumptions.size() > 0: incremental enabled? + std::vector<Expr> eassumptions = termVectorToExprs(assumptions); + CVC4::Result r = d_smtEngine->checkSat(eassumptions); + return Result(r); +} + +/** + * ( declare-const <symbol> <sort> ) + */ +Term Solver::declareConst(const std::string& symbol, Sort sort) const +{ + // CHECK: sort exists + return d_exprMgr->mkVar(symbol, *sort.d_type); +} + /** * ( declare-datatype <symbol> <datatype_decl> ) */ |