From 1a2d113fd62f1f8b362f907c0fd34c2adecdb1f1 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 6 Dec 2012 01:54:11 +0000 Subject: [PATCH] * tuple and record support in compatibility library (this commit was certified error- and warning-free by the test-and-commit script.) --- NEWS | 7 +++-- src/compat/cvc3_compat.cpp | 54 +++++++++++++++++++++++++++++--------- test/system/cvc3_main.cpp | 12 ++++----- 3 files changed, 53 insertions(+), 20 deletions(-) diff --git a/NEWS b/NEWS index a74093492..1790d6bd3 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,8 @@ This file contains a summary of important user-visible changes. -This is the first public release, CVC4 1.0. +Changes since 1.0 +================= --- Morgan Deters Sat, 01 Dec 2012 12:53:23 -0500 +* tuple and record support in the compatibility library + +-- Morgan Deters Wed, 05 Dec 2012 11:34:18 -0500 diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 02d76d351..2a8673451 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -1107,23 +1107,38 @@ Type ValidityChecker::tupleType(const std::vector& types) { } Type ValidityChecker::recordType(const std::string& field, const Type& type) { - Unimplemented("Records not supported by CVC4 yet (sorry!)"); + std::vector< std::pair > fields; + fields.push_back(std::make_pair(field, (const CVC4::Type&) type)); + return d_em->mkRecordType(CVC4::Record(fields)); } Type ValidityChecker::recordType(const std::string& field0, const Type& type0, const std::string& field1, const Type& type1) { - Unimplemented("Records not supported by CVC4 yet (sorry!)"); + std::vector< std::pair > fields; + fields.push_back(std::make_pair(field0, (const CVC4::Type&) type0)); + fields.push_back(std::make_pair(field1, (const CVC4::Type&) type1)); + return d_em->mkRecordType(CVC4::Record(fields)); } Type ValidityChecker::recordType(const std::string& field0, const Type& type0, const std::string& field1, const Type& type1, const std::string& field2, const Type& type2) { - Unimplemented("Records not supported by CVC4 yet (sorry!)"); + std::vector< std::pair > fields; + fields.push_back(std::make_pair(field0, (const CVC4::Type&) type0)); + fields.push_back(std::make_pair(field1, (const CVC4::Type&) type1)); + fields.push_back(std::make_pair(field2, (const CVC4::Type&) type2)); + return d_em->mkRecordType(CVC4::Record(fields)); } Type ValidityChecker::recordType(const std::vector& fields, const std::vector& types) { - Unimplemented("Records not supported by CVC4 yet (sorry!)"); + CVC4::CheckArgument(fields.size() == types.size() && fields.size() > 0, + "invalid vector length(s) in recordType()"); + std::vector< std::pair > fieldSpecs; + for(unsigned i = 0; i < fields.size(); ++i) { + fieldSpecs.push_back(std::make_pair(fields[i], (const CVC4::Type&) types[i])); + } + return d_em->mkRecordType(CVC4::Record(fieldSpecs)); } Type ValidityChecker::dataType(const std::string& name, @@ -1559,32 +1574,43 @@ Expr ValidityChecker::geExpr(const Expr& left, const Expr& right) { } Expr ValidityChecker::recordExpr(const std::string& field, const Expr& expr) { - Unimplemented("Records not supported by CVC4 yet (sorry!)"); + CVC4::Type t = recordType(field, expr.getType()); + return d_em->mkExpr(CVC4::kind::RECORD, d_em->mkConst(CVC4::RecordType(t).getRecord()), expr); } Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0, const std::string& field1, const Expr& expr1) { - Unimplemented("Records not supported by CVC4 yet (sorry!)"); + CVC4::Type t = recordType(field0, expr0.getType(), + field1, expr1.getType()); + return d_em->mkExpr(CVC4::kind::RECORD, d_em->mkConst(CVC4::RecordType(t).getRecord()), expr0, expr1); } Expr ValidityChecker::recordExpr(const std::string& field0, const Expr& expr0, const std::string& field1, const Expr& expr1, const std::string& field2, const Expr& expr2) { - Unimplemented("Records not supported by CVC4 yet (sorry!)"); + CVC4::Type t = recordType(field0, expr0.getType(), + field1, expr1.getType(), + field2, expr2.getType()); + return d_em->mkExpr(CVC4::kind::RECORD, d_em->mkConst(CVC4::RecordType(t).getRecord()), expr0, expr1, expr2); } Expr ValidityChecker::recordExpr(const std::vector& fields, const std::vector& exprs) { - Unimplemented("Records not supported by CVC4 yet (sorry!)"); + std::vector types; + for(unsigned i = 0; i < exprs.size(); ++i) { + types.push_back(exprs[i].getType()); + } + CVC4::Type t = recordType(fields, types); + return d_em->mkExpr(d_em->mkConst(CVC4::RecordType(t).getRecord()), *reinterpret_cast*>(&exprs)); } Expr ValidityChecker::recSelectExpr(const Expr& record, const std::string& field) { - Unimplemented("Records not supported by CVC4 yet (sorry!)"); + return d_em->mkExpr(d_em->mkConst(CVC4::RecordSelect(field)), record); } Expr ValidityChecker::recUpdateExpr(const Expr& record, const std::string& field, const Expr& newValue) { - Unimplemented("Records not supported by CVC4 yet (sorry!)"); + return d_em->mkExpr(d_em->mkConst(CVC4::RecordUpdate(field)), record, newValue); } Expr ValidityChecker::readExpr(const Expr& array, const Expr& index) { @@ -1935,12 +1961,16 @@ Expr ValidityChecker::tupleExpr(const std::vector& exprs) { } Expr ValidityChecker::tupleSelectExpr(const Expr& tuple, int index) { - Unimplemented("Tuples not supported by CVC4 yet (sorry!)"); + CVC4::CheckArgument(index >= 0 && index < tuple.getNumChildren(), + "invalid index in tuple select"); + return d_em->mkExpr(d_em->mkConst(CVC4::TupleSelect(index)), tuple); } Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index, const Expr& newValue) { - Unimplemented("Tuples not supported by CVC4 yet (sorry!)"); + CVC4::CheckArgument(index >= 0 && index < tuple.getNumChildren(), + "invalid index in tuple update"); + return d_em->mkExpr(d_em->mkConst(CVC4::TupleUpdate(index)), tuple, newValue); } Expr ValidityChecker::datatypeConsExpr(const std::string& constructor, const std::vector& args) { diff --git a/test/system/cvc3_main.cpp b/test/system/cvc3_main.cpp index 2afdc5ac6..e09a3f930 100644 --- a/test/system/cvc3_main.cpp +++ b/test/system/cvc3_main.cpp @@ -776,10 +776,10 @@ void test6() { newAssertion(vc1, ar_eq1); check(vc1, query1); - cout << "*** VC #2:" << endl; - newAssertion(vc2, vc2->importExpr(r1_eq)); - newAssertion(vc2, vc2->importExpr(ar_eq1)); - check(vc2, vc2->importExpr(query1)); + //cout << "*** VC #2:" << endl; + //newAssertion(vc2, vc2->importExpr(r1_eq)); + //newAssertion(vc2, vc2->importExpr(ar_eq1)); + //check(vc2, vc2->importExpr(query1)); } catch(const Exception& e) { exitStatus = 1; cout << "*** Exception caught in test6(): \n" << e << endl; @@ -2142,8 +2142,8 @@ int main(int argc, char** argv) cout << "\n}\n\ntest5(): {" << endl; test5(); } - //cout << "\n}\n\ntest6(): {" << endl; - //test6(); + cout << "\n}\n\ntest6(): {" << endl; + test6(); cout << "\n}\n\ntest7(): {" << endl; test7(); //cout << "\n}\n\ntest8(): {" << endl; -- 2.30.2