Skip to content

Commit

Permalink
Make ensureTermSort private (cvc5#8436)
Browse files Browse the repository at this point in the history
This method was used to correct a limitation in the old API regarding parsing decimals. It should not be a public API method.
  • Loading branch information
ajreynol authored Mar 29, 2022
1 parent 6c64864 commit cb49e01
Show file tree
Hide file tree
Showing 4 changed files with 13 additions and 53 deletions.
26 changes: 12 additions & 14 deletions src/api/cpp/cvc5.h
Original file line number Diff line number Diff line change
Expand Up @@ -4600,20 +4600,6 @@ class CVC5_EXPORT Solver
*/
void setOption(const std::string& option, const std::string& value) const;

/**
* If needed, convert this term to a given sort.
*
* @note The sort of the term must be convertible into the target sort.
* Currently only Int to Real conversions are supported.
*
* @warning This method is experimental and may change in future versions.
*
* @param t the term
* @param s the target sort
* @return the term wrapped into a sort conversion if needed
*/
Term ensureTermSort(const Term& t, const Sort& s) const;

/**
* Append \p symbol to the current list of universal variables.
*
Expand Down Expand Up @@ -4961,6 +4947,18 @@ class CVC5_EXPORT Solver
/** Check whether string s is a valid decimal integer. */
bool isValidInteger(const std::string& s) const;

/**
* If needed, convert this term to a given sort.
*
* The sort of the term must be convertible into the target sort.
* Currently only Int to Real conversions are supported.
*
* @param t the term
* @param s the target sort
* @return the term wrapped into a sort conversion if needed
*/
Term ensureTermSort(const Term& t, const Sort& s) const;

/**
* Check that the given term is a valid closed term, which can be used as an
* argument to, e.g., assert, get-value, block-model-values, etc.
Expand Down
20 changes: 0 additions & 20 deletions src/api/java/io/github/cvc5/api/Solver.java
Original file line number Diff line number Diff line change
Expand Up @@ -2508,26 +2508,6 @@ public void setOption(String option, String value)

private native void setOption(long pointer, String option, String value);

/**
* If needed, convert this term to a given sort.
*
* @apiNote The sort of the term must be convertible into the target sort.
* Currently only Int to Real conversions are supported.
*
* @apiNote This method is experimental and may change in future versions.
*
* @param t the term
* @param s the target sort
* @return the term wrapped into a sort conversion if needed
*/
public Term ensureTermSort(Term t, Sort s)
{
long termPointer = ensureTermSort(pointer, t.getPointer(), s.getPointer());
return new Term(this, termPointer);
}

private native long ensureTermSort(long pointer, long termPointer, long sortPointer);

/**
* Append \p symbol to the current list of universal variables.
* @param sort the sort of the universal variable
Expand Down
17 changes: 0 additions & 17 deletions src/api/java/jni/solver.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2385,23 +2385,6 @@ JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_setOption(
CVC5_JAVA_API_TRY_CATCH_END(env);
}

/*
* Class: io_github_cvc5_api_Solver
* Method: ensureTermSort
* Signature: (JJJ)J
*/
JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_ensureTermSort(
JNIEnv* env, jobject, jlong pointer, jlong termPointer, jlong sortPointer)
{
CVC5_JAVA_API_TRY_CATCH_BEGIN;
Solver* solver = reinterpret_cast<Solver*>(pointer);
Term* term = reinterpret_cast<Term*>(termPointer);
Sort* sort = reinterpret_cast<Sort*>(sortPointer);
Term* retPointer = new Term(solver->ensureTermSort(*term, *sort));
return reinterpret_cast<jlong>(retPointer);
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}

/*
* Class: io_github_cvc5_api_Solver
* Method: declareSygusVar
Expand Down
3 changes: 1 addition & 2 deletions src/parser/smt2/Smt2.g
Original file line number Diff line number Diff line change
Expand Up @@ -1706,8 +1706,7 @@ termAtomic[cvc5::api::Term& atomTerm]
| DECIMAL_LITERAL
{
std::string realStr = AntlrInput::tokenText($DECIMAL_LITERAL);
atomTerm = SOLVER->ensureTermSort(SOLVER->mkReal(realStr),
SOLVER->getRealSort());
atomTerm = SOLVER->mkReal(realStr);
}
// Constants using indexed identifiers, e.g. (_ +oo 8 24) (positive infinity
Expand Down

0 comments on commit cb49e01

Please sign in to comment.