diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-06-27 14:00:58 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-06-27 14:00:58 -0700 |
commit | bf40a0811328e294d98c07cf137f557aea68bdc8 (patch) | |
tree | 05305105f107a30867a5144da651dcd313a7767a /examples/api/sets-new.cpp | |
parent | d6c7967cfc7a9f8530f0de50f12f99bfc5f93da7 (diff) |
Header for new C++ API. (#1697)
Diffstat (limited to 'examples/api/sets-new.cpp')
-rw-r--r-- | examples/api/sets-new.cpp | 96 |
1 files changed, 96 insertions, 0 deletions
diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp new file mode 100644 index 000000000..be35bcc21 --- /dev/null +++ b/examples/api/sets-new.cpp @@ -0,0 +1,96 @@ +/********************* */ +/*! \file sets.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Kshitij Bansal + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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 sets with CVC4. + ** + ** A simple demonstration of reasoning about sets with CVC4. + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "api/cvc4cpp.h" + +using namespace std; +using namespace CVC4::api; + +int main() +{ + Solver slv; + + // Optionally, set the logic. We need at least UF for equality predicate, + // integers (LIA) and sets (FS). + slv.setLogic("QF_UFLIAFS"); + + // Produce models + slv.setOption("produce-models", "true"); + slv.setOption("output-language", "smt2"); + + Sort integer = slv.getIntegerSort(); + Sort set = slv.mkSetSort(integer); + + // Verify union distributions over intersection + // (A union B) intersection C = (A intersection C) union (B intersection C) + { + Term A = slv.mkVar("A", set); + Term B = slv.mkVar("B", set); + Term C = slv.mkVar("C", set); + + Term unionAB = slv.mkTerm(UNION, A, B); + Term lhs = slv.mkTerm(INTERSECTION, unionAB, C); + + Term intersectionAC = slv.mkTerm(INTERSECTION, A, C); + Term intersectionBC = slv.mkTerm(INTERSECTION, B, C); + Term rhs = slv.mkTerm(UNION, intersectionAC, intersectionBC); + + Term theorem = slv.mkTerm(EQUAL, lhs, rhs); + + cout << "CVC4 reports: " << theorem << " is " + << slv.checkValidAssuming(theorem) << "." << endl; + } + + // Verify emptset is a subset of any set + { + Term A = slv.mkVar("A", set); + Term emptyset = slv.mkEmptySet(set); + + Term theorem = slv.mkTerm(SUBSET, emptyset, A); + + cout << "CVC4 reports: " << theorem << " is " + << slv.checkValidAssuming(theorem) << "." << endl; + } + + // Find me an element in {1, 2} intersection {2, 3}, if there is one. + { + Term one = slv.mkInteger(1); + Term two = slv.mkInteger(2); + Term three = slv.mkInteger(3); + + Term singleton_one = slv.mkTerm(SINGLETON, one); + Term singleton_two = slv.mkTerm(SINGLETON, two); + Term singleton_three = slv.mkTerm(SINGLETON, three); + Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two); + Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three); + Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three); + + Term x = slv.mkVar("x", integer); + + Term e = slv.mkTerm(MEMBER, x, intersection); + + Result result = slv.checkSatAssuming(e); + cout << "CVC4 reports: " << e << " is " << result << "." << endl; + + if (result.isSat()) + { + cout << "For instance, " << slv.getValue(x) << " is a member." << endl; + } + } +} |