From 2ff7f9a5cde5faeb246b6c68de085ef008c107d2 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 30 Jul 2020 16:56:33 -0700 Subject: [PATCH] Python API: Add support for sequences (#4757) Commit 9678f58a7fedab4fc061761c58382f4023686108 added front end support for sequences. This commit extends that support to the Python API. It also adds simple C++ and Python examples that demonstrate how the API works for sequences. --- examples/api/CMakeLists.txt | 1 + examples/api/python/CMakeLists.txt | 1 + examples/api/python/sequences.py | 60 ++++++++++++++++++++++++++ examples/api/python/strings.py | 2 +- examples/api/sequences.cpp | 68 ++++++++++++++++++++++++++++++ examples/api/strings.cpp | 2 +- src/api/python/cvc4.pxd | 5 +++ src/api/python/cvc4.pxi | 26 ++++++++++++ src/prop/prop_engine.cpp | 2 +- test/unit/api/python/test_sort.py | 10 +++++ test/unit/api/python/test_term.py | 29 +++++++++++++ 11 files changed, 203 insertions(+), 3 deletions(-) create mode 100644 examples/api/python/sequences.py create mode 100644 examples/api/sequences.cpp diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt index 6421a3263..bd6361b5c 100644 --- a/examples/api/CMakeLists.txt +++ b/examples/api/CMakeLists.txt @@ -7,6 +7,7 @@ set(CVC4_EXAMPLES_API helloworld linear_arith sets + sequences strings sygus-fun sygus-grammar diff --git a/examples/api/python/CMakeLists.txt b/examples/api/python/CMakeLists.txt index 6e255c5b1..e3966fa2d 100644 --- a/examples/api/python/CMakeLists.txt +++ b/examples/api/python/CMakeLists.txt @@ -1,5 +1,6 @@ set(EXAMPLES_API_PYTHON exceptions + sequences ) find_package(PythonInterp REQUIRED) diff --git a/examples/api/python/sequences.py b/examples/api/python/sequences.py new file mode 100644 index 000000000..4498e5153 --- /dev/null +++ b/examples/api/python/sequences.py @@ -0,0 +1,60 @@ +#!/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))) diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py index 5c8e91997..58a6f6508 100755 --- a/examples/api/python/strings.py +++ b/examples/api/python/strings.py @@ -20,7 +20,7 @@ from pycvc4 import kinds 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 diff --git a/examples/api/sequences.cpp b/examples/api/sequences.cpp new file mode 100644 index 000000000..53bb584ce --- /dev/null +++ b/examples/api/sequences.cpp @@ -0,0 +1,68 @@ +/********************* */ +/*! \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 + +#include + +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; + } +} diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp index 6a0e10918..cd2a60cb1 100644 --- a/examples/api/strings.cpp +++ b/examples/api/strings.cpp @@ -25,7 +25,7 @@ int main() 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 diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index 940922052..eea263a96 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -132,6 +132,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": 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 + @@ -153,6 +154,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": 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 + @@ -246,6 +248,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": bint isRecord() except + bint isArray() except + bint isSet() except + + bint isSequence() except + bint isUninterpretedSort() except + bint isSortConstructor() except + bint isFirstClass() except + @@ -263,6 +266,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": Sort getArrayIndexSort() except + Sort getArrayElementSort() except + Sort getSetElementSort() except + + Sort getSequenceElementSort() except + string getUninterpretedSortName() except + bint isUninterpretedSortParameterized() except + vector[Sort] getUninterpretedSortParamSorts() except + @@ -293,6 +297,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": 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 + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 01660e206..133bd4660 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -459,6 +459,11 @@ cdef class Solver: 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()) @@ -613,6 +618,11 @@ cdef class Solver: " 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) @@ -1081,6 +1091,9 @@ cdef class Sort: def isSet(self): return self.csort.isSet() + def isSequence(self): + return self.csort.isSequence() + def isUninterpretedSort(self): return self.csort.isUninterpretedSort() @@ -1159,6 +1172,11 @@ cdef class Sort: 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() @@ -1282,6 +1300,14 @@ cdef class Term: 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() diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 2bf425f2b..c9d0b95b5 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -242,7 +242,7 @@ bool PropEngine::isSatLiteral(TNode node) const { 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); diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index 507aff2ae..cd40fc807 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -157,6 +157,16 @@ def testGetSetElementSort(): 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") diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index 43e541412..b135e4510 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -19,6 +19,13 @@ def test_get_kind(): 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() @@ -86,3 +93,25 @@ def test_is_const(): 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 -- 2.30.2