Home
last modified time | relevance | path

Searched refs:mkUninterpretedConst (Results 1 – 3 of 3) sorted by relevance

/dports/math/cvc4/CVC4-1.7/test/unit/api/
H A Dsolver_black.h321 d_solver->mkUninterpretedConst(d_solver->getBooleanSort(), 1)); in testMkUninterpretedConst()
322 TS_ASSERT_THROWS(d_solver->mkUninterpretedConst(Sort(), 1), in testMkUninterpretedConst()
/dports/math/cvc4/CVC4-1.7/src/api/
H A Dcvc4cpp.h2141 Term mkUninterpretedConst(Sort sort, int32_t index) const;
H A Dcvc4cpp.cpp2327 Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const in mkUninterpretedConst() function in CVC4::api::Solver