diff options
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cpp/cvc5.cpp | 32 | ||||
-rw-r--r-- | src/api/cpp/cvc5_kind.h | 44 | ||||
-rw-r--r-- | src/api/python/cvc5.pxd | 13 | ||||
-rw-r--r-- | src/api/python/cvc5.pxi | 84 |
4 files changed, 110 insertions, 63 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 0f2d5ad1b..668fc9382 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -4743,7 +4743,7 @@ Solver::Solver(Options* opts) } d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), d_originalOptions.get())); d_smtEngine->setSolver(this); - d_rng.reset(new Random(d_smtEngine->getOptions()[options::seed])); + d_rng.reset(new Random(d_smtEngine->getOptions().driver.seed)); resetStatistics(); } @@ -6452,7 +6452,7 @@ Result Solver::checkEntailed(const Term& term) const NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM(term); @@ -6468,7 +6468,7 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS(terms); @@ -6497,7 +6497,7 @@ Result Solver::checkSat(void) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; //////// all checks before this line @@ -6512,7 +6512,7 @@ Result Solver::checkSatAssuming(const Term& assumption) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort()); @@ -6528,7 +6528,7 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); CVC5_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0 - || d_smtEngine->getOptions()[options::incrementalSolving]) + || d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions, getBooleanSort()); @@ -6863,10 +6863,10 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const { CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC5_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot get unsat assumptions unless incremental solving is enabled " "(try --incremental)"; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatAssumptions]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatAssumptions) << "Cannot get unsat assumptions unless explicitly enabled " "(try --produce-unsat-assumptions)"; CVC5_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) @@ -6891,7 +6891,7 @@ std::vector<Term> Solver::getUnsatCore(void) const { CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatCores]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatCores) << "Cannot get unsat core unless explicitly enabled " "(try --produce-unsat-cores)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT) @@ -6925,7 +6925,7 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const { CVC5_API_TRY_CATCH_BEGIN; NodeManagerScope scope(getNodeManager()); - CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -6992,7 +6992,7 @@ Term Solver::getSeparationHeap() const d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) << "Cannot obtain separation logic expressions if not using the " "separation logic theory."; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get separation heap term unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -7011,7 +7011,7 @@ Term Solver::getSeparationNilTerm() const d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP)) << "Cannot obtain separation logic expressions if not using the " "separation logic theory."; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get separation nil term unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -7044,7 +7044,7 @@ void Solver::pop(uint32_t nscopes) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot pop when not solving incrementally (use --incremental)"; CVC5_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels()) << "Cannot pop beyond first pushed context"; @@ -7133,7 +7133,7 @@ void Solver::blockModel() const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -7148,7 +7148,7 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) @@ -7176,7 +7176,7 @@ void Solver::push(uint32_t nscopes) const { NodeManagerScope scope(getNodeManager()); CVC5_API_TRY_CATCH_BEGIN; - CVC5_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) + CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving) << "Cannot push when not solving incrementally (use --incremental)"; //////// all checks before this line for (uint32_t n = 0; n < nscopes; ++n) diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 4263eedb2..b4596e977 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -913,12 +913,8 @@ enum CVC5_EXPORT Kind : int32_t */ BITVECTOR_NEG, /** - * Unsigned division of two bit-vectors, truncating towards 0. - * - * Note: The semantics of this operator depends on `bv-div-zero-const` - * (default is true). Depending on the setting, a division by zero is - * treated as all ones (default, corresponds to SMT-LIB >=2.6) or an - * uninterpreted value (corresponds to SMT-LIB <2.6). + * Unsigned division of two bit-vectors, truncating towards 0. If the divisor + * is zero, the result is all ones. * * Parameters: * - 1..2: Terms of bit-vector sort (sorts must match) @@ -929,12 +925,8 @@ enum CVC5_EXPORT Kind : int32_t */ BITVECTOR_UDIV, /** - * Unsigned remainder from truncating division of two bit-vectors. - * - * Note: The semantics of this operator depends on `bv-div-zero-const` - * (default is true). Depending on the setting, if the modulus is zero, the - * result is either the dividend (default, corresponds to SMT-LIB >=2.6) or - * an uninterpreted value (corresponds to SMT-LIB <2.6). + * Unsigned remainder from truncating division of two bit-vectors. If the + * modulus is zero, the result is the dividend. * * Parameters: * - 1..2: Terms of bit-vector sort (sorts must match) @@ -945,13 +937,9 @@ enum CVC5_EXPORT Kind : int32_t */ BITVECTOR_UREM, /** - * Two's complement signed division of two bit-vectors. - * - * Note: The semantics of this operator depends on `bv-div-zero-const` - * (default is true). By default, the function returns all ones if the - * dividend is positive and one if the dividend is negative (corresponds to - * SMT-LIB >=2.6). If the option is disabled, a division by zero is treated - * as an uninterpreted value (corresponds to SMT-LIB <2.6). + * Two's complement signed division of two bit-vectors. If the divisor is + * zero and the dividend is positive, the result is all ones. If the divisor + * is zero and the dividend is negative, the result is one. * * Parameters: * - 1..2: Terms of bit-vector sort (sorts must match) @@ -962,13 +950,8 @@ enum CVC5_EXPORT Kind : int32_t */ BITVECTOR_SDIV, /** - * Two's complement signed remainder of two bit-vectors - * (sign follows dividend). - * - * Note: The semantics of this operator depends on `bv-div-zero-const` - * (default is true, corresponds to SMT-LIB >=2.6). Depending on the setting, - * if the modulus is zero, the result is either the dividend (default) or an - * uninterpreted value (corresponds to SMT-LIB <2.6). + * Two's complement signed remainder of two bit-vectors (sign follows + * dividend). If the modulus is zero, the result is the dividend. * * Parameters: * - 1..2: Terms of bit-vector sort (sorts must match) @@ -979,13 +962,8 @@ enum CVC5_EXPORT Kind : int32_t */ BITVECTOR_SREM, /** - * Two's complement signed remainder - * (sign follows divisor). - * - * Note: The semantics of this operator depends on `bv-div-zero-const` - * (default is on). Depending on the setting, if the modulus is zero, the - * result is either the dividend (default, corresponds to SMT-LIB >=2.6) or - * an uninterpreted value (corresponds to SMT-LIB <2.6). + * Two's complement signed remainder (sign follows divisor). If the modulus + * is zero, the result is the dividend. * * Parameters: * - 1..2: Terms of bit-vector sort (sorts must match) diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index fdcbfa997..2ad8cef5c 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -176,6 +176,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Sort mkTupleSort(const vector[Sort]& sorts) except + Term mkTerm(Op op) except + Term mkTerm(Op op, const vector[Term]& children) except + + Term mkTuple(const vector[Sort]& sorts, const vector[Term]& terms) except + Op mkOp(Kind kind) except + Op mkOp(Kind kind, Kind k) except + Op mkOp(Kind kind, const string& arg) except + @@ -388,6 +389,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term operator*() except + const_iterator begin() except + const_iterator end() except + + + bint isConstArray() except + bint isBooleanValue() except + bint getBooleanValue() except + bint isStringValue() except + @@ -398,6 +401,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": string getRealValue() except + bint isBitVectorValue() except + string getBitVectorValue(uint32_t base) except + + bint isAbstractValue() except + + string getAbstractValue() except + bint isFloatingPointPosZero() except + bint isFloatingPointNegZero() except + bint isFloatingPointPosInf() except + @@ -406,7 +411,15 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": bint isFloatingPointValue() except + tuple[uint32_t, uint32_t, Term] getFloatingPointValue() except + + bint isSetValue() except + + set[Term] getSetValue() except + + bint isSequenceValue() except + vector[Term] getSequenceValue() except + + bint isUninterpretedValue() except + + pair[Sort, int32_t] getUninterpretedValue() except + + bint isTupleValue() except + + vector[Term] getTupleValue() except + + cdef cppclass TermHashFunction: TermHashFunction() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 25ded76bb..8599a1cd1 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -658,6 +658,19 @@ cdef class Solver: term.cterm = self.csolver.mkTerm((<Op?> op).cop, v) return term + def mkTuple(self, sorts, terms): + cdef vector[c_Sort] csorts + cdef vector[c_Term] cterms + + for s in sorts: + csorts.push_back((<Sort?> s).csort) + for s in terms: + cterms.push_back((<Term?> s).cterm) + cdef Term result = Term(self) + result.cterm = self.csolver.mkTuple(csorts, cterms) + return result + + def mkOp(self, kind k, arg0=None, arg1 = None): ''' Supports the following uses: @@ -1609,19 +1622,6 @@ cdef class Term: def isNull(self): return self.cterm.isNull() - def getConstArrayBase(self): - cdef Term term = Term(self.solver) - term.cterm = self.cterm.getConstArrayBase() - return term - - def getSequenceValue(self): - elems = [] - for e in self.cterm.getSequenceValue(): - term = Term(self.solver) - term.cterm = e - elems.append(term) - return elems - def notTerm(self): cdef Term term = Term(self.solver) term.cterm = self.cterm.notTerm() @@ -1657,6 +1657,14 @@ cdef class Term: term.cterm = self.cterm.iteTerm(then_t.cterm, else_t.cterm) return term + def isConstArray(self): + return self.cterm.isConstArray() + + def getConstArrayBase(self): + cdef Term term = Term(self.solver) + term.cterm = self.cterm.getConstArrayBase() + return term + def isBooleanValue(self): return self.cterm.isBooleanValue() @@ -1673,7 +1681,12 @@ cdef class Term: def isIntegerValue(self): return self.cterm.isIntegerValue() - + def isAbstractValue(self): + return self.cterm.isAbstractValue() + + def getAbstractValue(self): + return self.cterm.getAbstractValue().decode() + def isFloatingPointPosZero(self): return self.cterm.isFloatingPointPosZero() @@ -1698,6 +1711,49 @@ cdef class Term: term.cterm = get2(t) return (get0(t), get1(t), term) + def isSetValue(self): + return self.cterm.isSetValue() + + def getSetValue(self): + elems = set() + for e in self.cterm.getSetValue(): + term = Term(self.solver) + term.cterm = e + elems.add(term) + return elems + + def isSequenceValue(self): + return self.cterm.isSequenceValue() + + def getSequenceValue(self): + elems = [] + for e in self.cterm.getSequenceValue(): + term = Term(self.solver) + term.cterm = e + elems.append(term) + return elems + + def isUninterpretedValue(self): + return self.cterm.isUninterpretedValue() + + def getUninterpretedValue(self): + cdef pair[c_Sort, int32_t] p = self.cterm.getUninterpretedValue() + cdef Sort sort = Sort(self.solver) + sort.csort = p.first + i = p.second + return (sort, i) + + def isTupleValue(self): + return self.cterm.isTupleValue() + + def getTupleValue(self): + elems = [] + for e in self.cterm.getTupleValue(): + term = Term(self.solver) + term.cterm = e + elems.append(term) + return elems + def getIntegerValue(self): return int(self.cterm.getIntegerValue().decode()) |