diff options
Diffstat (limited to 'src/api/cpp/cvc5.cpp')
| -rw-r--r-- | src/api/cpp/cvc5.cpp | 78 |
1 files changed, 3 insertions, 75 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 49ef2336c..310ff3128 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -3725,7 +3725,7 @@ void Grammar::addAnyVariable(const Term& ntSymbol) } /** - * this function concatinates the outputs of calling f on each element between + * This function concatenates the outputs of calling f on each element between * first and last, seperated by sep. * @param first the beginning of the range * @param last the end of the range @@ -5845,9 +5845,6 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const /* SMT-LIB commands */ /* -------------------------------------------------------------------------- */ -/** - * ( assert <term> ) - */ void Solver::assertFormula(const Term& term) const { CVC4_API_TRY_CATCH_BEGIN; @@ -5859,9 +5856,6 @@ void Solver::assertFormula(const Term& term) const CVC4_API_TRY_CATCH_END; } -/** - * ( check-sat ) - */ Result Solver::checkSat(void) const { CVC4_API_TRY_CATCH_BEGIN; @@ -5877,9 +5871,6 @@ Result Solver::checkSat(void) const CVC4_API_TRY_CATCH_END; } -/** - * ( check-sat-assuming ( <prop_literal> ) ) - */ Result Solver::checkSatAssuming(const Term& assumption) const { CVC4_API_TRY_CATCH_BEGIN; @@ -5896,9 +5887,6 @@ Result Solver::checkSatAssuming(const Term& assumption) const CVC4_API_TRY_CATCH_END; } -/** - * ( check-sat-assuming ( <prop_literal>* ) ) - */ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const { CVC4_API_TRY_CATCH_BEGIN; @@ -5920,9 +5908,6 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const CVC4_API_TRY_CATCH_END; } -/** - * ( declare-datatype <symbol> <datatype_decl> ) - */ Sort Solver::declareDatatype( const std::string& symbol, const std::vector<DatatypeConstructorDecl>& ctors) const @@ -5942,9 +5927,6 @@ Sort Solver::declareDatatype( CVC4_API_TRY_CATCH_END; } -/** - * ( declare-fun <symbol> ( <sort>* ) <sort> ) - */ Term Solver::declareFun(const std::string& symbol, const std::vector<Sort>& sorts, const Sort& sort) const @@ -5965,9 +5947,6 @@ Term Solver::declareFun(const std::string& symbol, CVC4_API_TRY_CATCH_END; } -/** - * ( declare-sort <symbol> <numeral> ) - */ Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const { CVC4_API_TRY_CATCH_BEGIN; @@ -5981,9 +5960,6 @@ Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const CVC4_API_TRY_CATCH_END; } -/** - * ( define-fun <function_def> ) - */ Term Solver::defineFun(const std::string& symbol, const std::vector<Term>& bound_vars, const Sort& sort, @@ -6051,9 +6027,6 @@ Term Solver::defineFun(const Term& fun, CVC4_API_TRY_CATCH_END; } -/** - * ( define-fun-rec <function_def> ) - */ Term Solver::defineFunRec(const std::string& symbol, const std::vector<Term>& bound_vars, const Sort& sort, @@ -6142,9 +6115,6 @@ Term Solver::defineFunRec(const Term& fun, CVC4_API_TRY_CATCH_END; } -/** - * ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) ) - */ void Solver::defineFunsRec(const std::vector<Term>& funs, const std::vector<std::vector<Term>>& bound_vars, const std::vector<Term>& terms, @@ -6210,17 +6180,11 @@ void Solver::defineFunsRec(const std::vector<Term>& funs, CVC4_API_TRY_CATCH_END; } -/** - * ( echo <std::string> ) - */ void Solver::echo(std::ostream& out, const std::string& str) const { out << str; } -/** - * ( get-assertions ) - */ std::vector<Term> Solver::getAssertions(void) const { CVC4_API_TRY_CATCH_BEGIN; @@ -6239,9 +6203,6 @@ std::vector<Term> Solver::getAssertions(void) const CVC4_API_TRY_CATCH_END; } -/** - * ( get-info <info_flag> ) - */ std::string Solver::getInfo(const std::string& flag) const { CVC4_API_TRY_CATCH_BEGIN; @@ -6253,9 +6214,6 @@ std::string Solver::getInfo(const std::string& flag) const CVC4_API_TRY_CATCH_END; } -/** - * ( get-option <keyword> ) - */ std::string Solver::getOption(const std::string& option) const { CVC4_API_TRY_CATCH_BEGIN; @@ -6266,9 +6224,6 @@ std::string Solver::getOption(const std::string& option) const CVC4_API_TRY_CATCH_END; } -/** - * ( get-unsat-assumptions ) - */ std::vector<Term> Solver::getUnsatAssumptions(void) const { CVC4_API_TRY_CATCH_BEGIN; @@ -6297,9 +6252,6 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const CVC4_API_TRY_CATCH_END; } -/** - * ( get-unsat-core ) - */ std::vector<Term> Solver::getUnsatCore(void) const { CVC4_API_TRY_CATCH_BEGIN; @@ -6324,9 +6276,6 @@ std::vector<Term> Solver::getUnsatCore(void) const CVC4_API_TRY_CATCH_END; } -/** - * ( get-value ( <term> ) ) - */ Term Solver::getValue(const Term& term) const { CVC4_API_TRY_CATCH_BEGIN; @@ -6337,9 +6286,6 @@ Term Solver::getValue(const Term& term) const CVC4_API_TRY_CATCH_END; } -/** - * ( get-value ( <term>+ ) ) - */ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const { CVC4_API_TRY_CATCH_BEGIN; @@ -6441,9 +6387,6 @@ Term Solver::getSeparationNilTerm() const CVC4_API_TRY_CATCH_END; } -/** - * ( pop <numeral> ) - */ void Solver::pop(uint32_t nscopes) const { NodeManagerScope scope(getNodeManager()); @@ -6576,9 +6519,6 @@ void Solver::printInstantiations(std::ostream& out) const CVC4_API_TRY_CATCH_END; } -/** - * ( push <numeral> ) - */ void Solver::push(uint32_t nscopes) const { NodeManagerScope scope(getNodeManager()); @@ -6594,9 +6534,6 @@ void Solver::push(uint32_t nscopes) const CVC4_API_TRY_CATCH_END; } -/** - * ( reset-assertions ) - */ void Solver::resetAssertions(void) const { CVC4_API_TRY_CATCH_BEGIN; @@ -6606,9 +6543,6 @@ void Solver::resetAssertions(void) const CVC4_API_TRY_CATCH_END; } -/** - * ( set-info <attribute> ) - */ void Solver::setInfo(const std::string& keyword, const std::string& value) const { CVC4_API_TRY_CATCH_BEGIN; @@ -6635,9 +6569,6 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const CVC4_API_TRY_CATCH_END; } -/** - * ( set-logic <symbol> ) - */ void Solver::setLogic(const std::string& logic) const { CVC4_API_TRY_CATCH_BEGIN; @@ -6650,9 +6581,6 @@ void Solver::setLogic(const std::string& logic) const CVC4_API_TRY_CATCH_END; } -/** - * ( set-option <option> ) - */ void Solver::setOption(const std::string& option, const std::string& value) const { @@ -6881,13 +6809,13 @@ void Solver::printSynthSolution(std::ostream& out) const CVC4_API_TRY_CATCH_END; } -/** +/* * !!! This is only temporarily available until the parser is fully migrated to * the new API. !!! */ SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); } -/** +/* * !!! This is only temporarily available until the parser is fully migrated to * the new API. !!! */ |