helloworld
linear_arith
sets
+ sequences
strings
sygus-fun
sygus-grammar
set(EXAMPLES_API_PYTHON
exceptions
+ sequences
)
find_package(PythonInterp REQUIRED)
--- /dev/null
+#!/usr/bin/env python
+
+#####################
+#! \file sequences.py
+## \verbatim
+## Top contributors (to current version):
+## Andres Noetzli
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory) and their institutional affiliations.
+## All rights reserved. See the file COPYING in the top-level source
+## directory for licensing information.\endverbatim
+##
+## \brief A simple demonstration of the solving capabilities of the CVC4
+## strings solver through the Python API. This is a direct translation
+## of sequences.cpp.
+import pycvc4
+from pycvc4 import kinds
+
+if __name__ == "__main__":
+ slv = pycvc4.Solver()
+ # Set the logic
+ slv.setLogic("QF_SLIA")
+ # Produce models
+ slv.setOption("produce-models", "true")
+ # The option strings-exp is needed
+ slv.setOption("strings-exp", "true")
+ # Set output language to SMTLIB2
+ slv.setOption("output-language", "smt2")
+
+ # Sequence sort
+ int_seq = slv.mkSequenceSort(slv.getIntegerSort())
+
+ # Sequence variables
+ x = slv.mkConst(int_seq, "x")
+ y = slv.mkConst(int_seq, "y")
+
+ # Empty sequence
+ empty = slv.mkEmptySequence(slv.getIntegerSort())
+ # Sequence concatenation: x.y.empty
+ concat = slv.mkTerm(kinds.SeqConcat, x, y, empty)
+ # Sequence length: |x.y.empty|
+ concat_len = slv.mkTerm(kinds.SeqLength, concat)
+ # |x.y.empty| > 1
+ formula1 = slv.mkTerm(kinds.Gt, concat_len, slv.mkReal(1))
+ # Sequence unit: seq(1)
+ unit = slv.mkTerm(kinds.SeqUnit, slv.mkReal(1))
+ # x = seq(1)
+ formula2 = slv.mkTerm(kinds.Equal, x, unit)
+
+ # Make a query
+ q = slv.mkTerm(kinds.And, formula1, formula2)
+
+ # Check satisfiability
+ result = slv.checkSatAssuming(q)
+ print("CVC4 reports:", q, "is", result)
+
+ if result:
+ print("x = {}".format(slv.getValue(x)))
+ print("y = {}".format(slv.getValue(y)))
if __name__ == "__main__":
slv = pycvc4.Solver()
# Set the logic
- slv.setLogic("S")
+ slv.setLogic("QF_SLIA")
# Produce models
slv.setOption("produce-models", "true")
# The option strings-exp is needed
--- /dev/null
+/********************* */
+/*! \file sequences.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Reasoning about sequences with CVC4 via C++ API.
+ **
+ ** A simple demonstration of reasoning about sequences with CVC4 via C++ API.
+ **/
+
+#include <cvc4/api/cvc4cpp.h>
+
+#include <iostream>
+
+using namespace CVC4::api;
+
+int main()
+{
+ Solver slv;
+
+ // Set the logic
+ slv.setLogic("QF_SLIA");
+ // Produce models
+ slv.setOption("produce-models", "true");
+ // The option strings-exp is needed
+ slv.setOption("strings-exp", "true");
+ // Set output language to SMTLIB2
+ slv.setOption("output-language", "smt2");
+
+ // Sequence sort
+ Sort intSeq = slv.mkSequenceSort(slv.getIntegerSort());
+
+ // Sequence variables
+ Term x = slv.mkConst(intSeq, "x");
+ Term y = slv.mkConst(intSeq, "y");
+
+ // Empty sequence
+ Term empty = slv.mkEmptySequence(slv.getIntegerSort());
+ // Sequence concatenation: x.y.empty
+ Term concat = slv.mkTerm(SEQ_CONCAT, x, y, empty);
+ // Sequence length: |x.y.empty|
+ Term concat_len = slv.mkTerm(SEQ_LENGTH, concat);
+ // |x.y.empty| > 1
+ Term formula1 = slv.mkTerm(GT, concat_len, slv.mkReal(1));
+ // Sequence unit: seq(1)
+ Term unit = slv.mkTerm(SEQ_UNIT, slv.mkReal(1));
+ // x = seq(1)
+ Term formula2 = slv.mkTerm(EQUAL, x, unit);
+
+ // Make a query
+ Term q = slv.mkTerm(AND, formula1, formula2);
+
+ // check sat
+ Result result = slv.checkSatAssuming(q);
+ std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl;
+
+ if (result.isSat())
+ {
+ std::cout << " x = " << slv.getValue(x) << std::endl;
+ std::cout << " y = " << slv.getValue(y) << std::endl;
+ }
+}
Solver slv;
// Set the logic
- slv.setLogic("S");
+ slv.setLogic("QF_SLIA");
// Produce models
slv.setOption("produce-models", "true");
// The option strings-exp is needed
Sort mkPredicateSort(const vector[Sort]& sorts) except +
Sort mkRecordSort(const vector[pair[string, Sort]]& fields) except +
Sort mkSetSort(Sort elemSort) except +
+ Sort mkSequenceSort(Sort elemSort) except +
Sort mkUninterpretedSort(const string& symbol) except +
Sort mkSortConstructorSort(const string& symbol, size_t arity) except +
Sort mkTupleSort(const vector[Sort]& sorts) except +
Term mkSepNil(Sort sort) except +
Term mkString(const string& s) except +
Term mkString(const vector[unsigned]& s) except +
+ Term mkEmptySequence(Sort sort) except +
Term mkUniverseSet(Sort sort) except +
Term mkBitVector(uint32_t size) except +
Term mkBitVector(uint32_t size, uint64_t val) except +
bint isRecord() except +
bint isArray() except +
bint isSet() except +
+ bint isSequence() except +
bint isUninterpretedSort() except +
bint isSortConstructor() except +
bint isFirstClass() except +
Sort getArrayIndexSort() except +
Sort getArrayElementSort() except +
Sort getSetElementSort() except +
+ Sort getSequenceElementSort() except +
string getUninterpretedSortName() except +
bint isUninterpretedSortParameterized() except +
vector[Sort] getUninterpretedSortParamSorts() except +
bint isNull() except +
bint isConst() except +
Term getConstArrayBase() except +
+ vector[Term] getConstSequenceElements() except +
Term notTerm() except +
Term andTerm(const Term& t) except +
Term orTerm(const Term& t) except +
sort.csort = self.csolver.mkSetSort(elemSort.csort)
return sort
+ def mkSequenceSort(self, Sort elemSort):
+ cdef Sort sort = Sort()
+ sort.csort = self.csolver.mkSequenceSort(elemSort.csort)
+ return sort
+
def mkUninterpretedSort(self, str name):
cdef Sort sort = Sort()
sort.csort = self.csolver.mkUninterpretedSort(name.encode())
" but got: {}".format(str_or_vec))
return term
+ def mkEmptySequence(self, Sort sort):
+ cdef Term term = Term()
+ term.cterm = self.csolver.mkEmptySequence(sort.csort)
+ return term
+
def mkUniverseSet(self, Sort sort):
cdef Term term = Term()
term.cterm = self.csolver.mkUniverseSet(sort.csort)
def isSet(self):
return self.csort.isSet()
+ def isSequence(self):
+ return self.csort.isSequence()
+
def isUninterpretedSort(self):
return self.csort.isUninterpretedSort()
sort.csort = self.csort.getSetElementSort()
return sort
+ def getSequenceElementSort(self):
+ cdef Sort sort = Sort()
+ sort.csort = self.csort.getSequenceElementSort()
+ return sort
+
def getUninterpretedSortName(self):
return self.csort.getUninterpretedSortName().decode()
term.cterm = self.cterm.getConstArrayBase()
return term
+ def getConstSequenceElements(self):
+ elems = []
+ for e in self.cterm.getConstSequenceElements():
+ term = Term()
+ term.cterm = e
+ elems.append(term)
+ return elems
+
def notTerm(self):
cdef Term term = Term()
term.cterm = self.cterm.notTerm()
bool PropEngine::hasValue(TNode node, bool& value) const {
Assert(node.getType().isBoolean());
- Assert(d_cnfStream->hasLiteral(node));
+ Assert(d_cnfStream->hasLiteral(node)) << node;
SatLiteral lit = d_cnfStream->getLiteral(node);
with pytest.raises(Exception):
bvSort.getSetElementSort()
+def testGetSequenceElementSort():
+ solver = pycvc4.Solver()
+ seqSort = solver.mkSequenceSort(solver.getIntegerSort())
+ seqSort.getSequenceElementSort()
+ bvSort = solver.mkBitVectorSort(32)
+ assert not bvSort.isSequence()
+
+ with pytest.raises(Exception):
+ bvSort.getSetElementSort()
+
def testGetUninterpretedSortName():
solver = pycvc4.Solver()
uSort = solver.mkUninterpretedSort("u")
fx = solver.mkTerm(kinds.ApplyUf, f, x)
assert fx.getKind() == kinds.ApplyUf
+ # Sequence kinds do not exist internally, test that the API properly
+ # converts them back.
+ seqsort = solver.mkSequenceSort(intsort)
+ s = solver.mkConst(seqsort, 's')
+ ss = solver.mkTerm(kinds.SeqConcat, s, s)
+ assert ss.getKind() == kinds.SeqConcat
+
def test_eq():
solver = pycvc4.Solver()
assert one.isConst()
assert not xpone.isConst()
assert not onepone.isConst()
+
+def test_const_sequence_elements():
+ solver = pycvc4.Solver()
+ realsort = solver.getRealSort()
+ seqsort = solver.mkSequenceSort(realsort)
+ s = solver.mkEmptySequence(seqsort)
+
+ assert s.isConst()
+
+ assert s.getKind() == kinds.ConstSequence
+ # empty sequence has zero elements
+ cs = s.getConstSequenceElements()
+ assert len(cs) == 0
+
+ # A seq.unit app is not a constant sequence (regardless of whether it is
+ # applied to a constant).
+ su = solver.mkTerm(kinds.SeqUnit, solver.mkReal(1))
+ try:
+ su.getConstSequenceElements()
+ assert False
+ except:
+ assert True
projects / cvc5.git / commitdiff