* tuple and record support in compatibility library

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/NEWS b/NEWS
index a740934926750196c0d48a12a73eb4c2779e0275..1790d6bd368a8470356b6655c1777a74ce563967 100644 (file)
--- 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 <mdeters@cs.nyu.edu>  Sat, 01 Dec 2012 12:53:23 -0500
+* tuple and record support in the compatibility library
+
+-- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 05 Dec 2012 11:34:18 -0500

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 02d76d351b902a84aecf2d81213c521f5e9fffa3..2a86734513551d5799eb5ecfa785c30d7bcd4347 100644 (file)
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1107,23 +1107,38 @@ Type ValidityChecker::tupleType(const std::vector<Type>& types) {
 }
 
 Type ValidityChecker::recordType(const std::string& field, const Type& type) {
-  Unimplemented("Records not supported by CVC4 yet (sorry!)");
+  std::vector< std::pair<std::string, CVC4::Type> > 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<std::string, CVC4::Type> > 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<std::string, CVC4::Type> > 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<std::string>& fields,
                                  const std::vector<Type>& 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<std::string, CVC4::Type> > 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<std::string>& fields,
                                  const std::vector<Expr>& exprs) {
-  Unimplemented("Records not supported by CVC4 yet (sorry!)");
+  std::vector<Type> 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<const vector<CVC4::Expr>*>(&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<Expr>& 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<Expr>& args) {

diff --git a/test/system/cvc3_main.cpp b/test/system/cvc3_main.cpp
index 2afdc5ac6547f333627ee00f43bb83460fac4534..e09a3f9302faf3b5edc6057d51969b37ea45c285 100644 (file)
--- 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;