diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-07-30 16:56:33 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-30 16:56:33 -0700 |
commit | 2ff7f9a5cde5faeb246b6c68de085ef008c107d2 (patch) | |
tree | 9e1f1c4d49c8465584469e15c24fbadb373887db /examples | |
parent | 3e18cd977b6e8d9729a4aa0f4cfc12710d21c863 (diff) |
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.
Diffstat (limited to 'examples')
-rw-r--r-- | examples/api/CMakeLists.txt | 1 | ||||
-rw-r--r-- | examples/api/python/CMakeLists.txt | 1 | ||||
-rw-r--r-- | examples/api/python/sequences.py | 60 | ||||
-rwxr-xr-x | examples/api/python/strings.py | 2 | ||||
-rw-r--r-- | examples/api/sequences.cpp | 68 | ||||
-rw-r--r-- | examples/api/strings.cpp | 2 |
6 files changed, 132 insertions, 2 deletions
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 <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; + } +} 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 |