From f7ebbd30653cffa3412b914f5813302bd2101578 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 22 Jan 2019 10:55:13 -0800 Subject: New README (markdown). (#2797) --- README | 102 ---------------------------------------------- README.md | 138 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 138 insertions(+), 102 deletions(-) delete mode 100644 README create mode 100644 README.md diff --git a/README b/README deleted file mode 100644 index 0a8a37879..000000000 --- a/README +++ /dev/null @@ -1,102 +0,0 @@ -This is CVC4 release version 1.6. For build and installation notes, -please see the INSTALL file included with this distribution. - -The project leaders are Clark Barrett (Stanford University) and Cesare -Tinelli (The University of Iowa). For a full list of authors, please -refer to the AUTHORS file in the source distribution. - -CVC4 is a tool for determining the satisfiability of a first order -formula modulo a first order theory (or a combination of such -theories). It is the fourth in the Cooperating Validity Checker -family of tools (CVC, CVC Lite, CVC3) but does not directly -incorporate code from any previous version. - -CVC4 is intended to be an open and extensible SMT engine. It can be -used as a stand-alone tool or as a library. It has been designed to -increase the performance and reduce the memory overhead of its -predecessors. It is written entirely in C++ and is released under an -open-source software license (see the file COPYING in the source -distribution). - -*** Getting started with CVC4 - -For help installing CVC4, see the INSTALL file that comes with this -distribution. - -We recommend that you visit our CVC4 tutorials online at: - - http://cvc4.cs.stanford.edu/wiki/Tutorials - -for help getting started using CVC4. - -*** Contributing to the CVC4 project - -We are always happy to hear feedback from our users: - -* if you need help with using CVC4, please refer to - http://cvc4.stanford.edu/#Technical_Support. - -* if you need to report a bug with CVC4, or make a feature request, - please visit our bugtracker at https://github.com/CVC4/CVC4/issues or - write to the cvc-bugs@cs.stanford.edu mailing list. We are very - grateful for bug reports, as they help us improve CVC4, and patches - are generally reviewed and accepted quickly. - -* if you are using CVC4 in your work, or incorporating it into - software of your own, we'd like to invite you to leave a description - and link to your project/software on our "Third Party Applications" - page at - http://cvc4.cs.stanford.edu/wiki/Public:Third_Party_Applications - -* if you are interested in contributing code (for example, a new - decision procedure implementation) to the CVC4 project, please - contact one of the project leaders. We'd be happy to point you to - some internals documentation to help you out. - -Thank you for using CVC4! - -*** The History of CVC4 - -The Cooperating Validity Checker series has a long history. The -Stanford Validity Checker (SVC) came first in 1996, incorporating -theories and its own SAT solver. Its successor, the Cooperating -Validity Checker (CVC), had a more optimized internal design, produced -proofs, used the Chaff SAT solver, and featured a number of usability -enhancements. Its name comes from the cooperative nature of decision -procedures in Nelson-Oppen theory combination, which share amongst -each other equalities between shared terms. CVC Lite, first made -available in 2003, was a rewrite of CVC that attempted to make CVC -more flexible (hence the "lite") while extending the feature set: CVC -Lite supported quantifiers where its predecessors did not. CVC3 was a -major overhaul of portions of CVC Lite: it added better decision -procedure implementations, added support for using MiniSat in the -core, and had generally better performance. - -CVC4 is the new version, the fifth generation of this validity checker -line that is now celebrating twenty-one years of heritage. It -represents a complete re-evaluation of the core architecture to be -both performant and to serve as a cutting-edge research vehicle for -the next several years. Rather than taking CVC3 and redesigning -problem parts, we've taken a clean-room approach, starting from -scratch. Before using any designs from CVC3, we have thoroughly -scrutinized, vetted, and updated them. Many parts of CVC4 bear only a -superficial resemblance, if any, to their correspondent in CVC3. - -However, CVC4 is fundamentally similar to CVC3 and many other modern -SMT solvers: it is a DPLL(T) solver, with a SAT solver at its core and -a delegation path to different decision procedure implementations, -each in charge of solving formulas in some background theory. - -The re-evaluation and ground-up rewrite was necessitated, we felt, by -the performance characteristics of CVC3. CVC3 has many useful -features, but some core aspects of the design led to high memory use, -and the use of heavyweight computation (where more nimble engineering -approaches could suffice) makes CVC3 a much slower prover than other -tools. As these designs are central to CVC3, a new version was -preferable to a selective re-engineering, which would have ballooned -in short order. - -*** For more information - -More information about CVC4 is available at: -http://cvc4.cs.stanford.edu/ diff --git a/README.md b/README.md new file mode 100644 index 000000000..153118c6b --- /dev/null +++ b/README.md @@ -0,0 +1,138 @@ +[![License: BSD]( + https://img.shields.io/badge/License-BSD%203--Clause-blue.svg)]( + https://opensource.org/licenses/BSD-3-Clause) +[![Build Status]( + https://travis-ci.org/CVC4/CVC4.svg?branch=master)]( + https://travis-ci.org/CVC4/CVC4) + +CVC4 +=============================================================================== + +CVC4 is a tool for determining the satisfiability of a first order formula +modulo a first order theory (or a combination of such theories). It is the +fourth in the Cooperating Validity Checker family of tools (CVC, CVC Lite, +CVC3) but does not directly incorporate code from any previous version. + +CVC4 is intended to be an open and extensible SMT engine. It can be used as a +stand-alone tool or as a library. It has been designed to increase the +performance and reduce the memory overhead of its predecessors. It is written +entirely in C++ and is released under an open-source software license (see file +[COPYING](https://github.com/CVC4/CVC4/blob/master/COPYING)). + + +Website +------------------------------------------------------------------------------- + +More information about CVC4 is available at: +http://cvc4.cs.stanford.edu/ + +Download +------------------------------------------------------------------------------- + +The latest version of CVC4 is available on GitHub: +https://github.com/CVC4/CVC4 + +Source tar balls and binaries for releases and latest stable builds of the +[master branch](https://github.com/CVC4/CVC4) on GitHub can be +found [here](http://cvc4.cs.stanford.edu/downloads). + + +Build and Dependencies +------------------------------------------------------------------------------- + +CVC4 can be built on Linux and macOS. For Windows, CVC4 can be cross-compiled +using Mingw-w64. + +For detailed build and installation instructions on these platforms, +see file [INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md). + + +Getting Started +------------------------------------------------------------------------------- + +We recommend that you visit our CVC4 tutorials online at: + + http://cvc4.cs.stanford.edu/wiki/Tutorials + +for help getting started using CVC4. + + +Contributing +------------------------------------------------------------------------------- + +We are always happy to hear feedback from our users: + +* if you need help with using CVC4, please refer to + [http://cvc4.stanford.edu/#Technical_Support](http://cvc4.stanford.edu/#Technical_Support). + +* if you need to report a bug with CVC4, or make a feature request, please + visit our bugtracker at our + [GitHub issues](https://github.com/CVC4/CVC4/issues) page or write to the + cvc-bugs@cs.stanford.edu mailing list. We are very grateful for bug reports, + as they help us improve CVC4, and patches are generally reviewed and accepted + quickly. + +* if you are using CVC4 in your work, or incorporating it into software of your + own, we'd like to invite you to leave a description and link to your + project/software on our [Third Party Applications](http://cvc4.cs.stanford.edu/wiki/Public:Third_Party_Applications). + +* if you are interested in contributing code (for example, a new + decision procedure implementation) to the CVC4 project, please + contact one of the [project leaders](#project_leaders). + We'd be happy to point you to some internal documentation to help you out. + +Thank you for using CVC4! + + +Project Leaders +------------------------------------------------------------------------------- + +* [Clark Barrett](http://theory.stanford.edu/~barrett/) (Stanford University) +* [Cesare Tinelli](http://homepage.cs.uiowa.edu/~tinelli/) (The University of Iowa) + + +Authors +------------------------------------------------------------------------------- + +For a full list of authors, please refer to the +[AUTHORS](https://github.com/CVC4/CVC4/blob/master/AUTHORS) file. + +History +------------------------------------------------------------------------------- + +The Cooperating Validity Checker series has a long history. The Stanford +Validity Checker (SVC) came first in 1996, incorporating theories and its own +SAT solver. Its successor, the Cooperating Validity Checker (CVC), had a more +optimized internal design, produced proofs, used the Chaff SAT solver, and +featured a number of usability enhancements. Its name comes from the +cooperative nature of decision procedures in Nelson-Oppen theory combination, +which share amongst each other equalities between shared terms. + +CVC Lite, first made available in 2003, was a rewrite of CVC that attempted to +make CVC more flexible (hence the "lite") while extending the feature set: CVC +Lite supported quantifiers where its predecessors did not. + +CVC3 was a major overhaul of portions of CVC Lite: it added better decision +procedure implementations, added support for using MiniSat in the core, and had +generally better performance. + +CVC4 is the fifth generation of this validity checker line. It represents a +complete re-evaluation of the core architecture to be both performant and to +serve as a cutting-edge research vehicle for the next several years. Rather +than taking CVC3 and redesigning problem parts, we've taken a clean-room +approach, starting from scratch. Before using any designs from CVC3, we have +thoroughly scrutinized, vetted, and updated them. Many parts of CVC4 bear only +a superficial resemblance, if any, to their correspondent in CVC3. + +However, CVC4 is fundamentally similar to CVC3 and many other modern SMT +solvers: it is a DPLL(T) solver, with a SAT solver at its core and a delegation +path to different decision procedure implementations, each in charge of solving +formulas in some background theory. + +The re-evaluation and ground-up rewrite was necessitated, we felt, by the +performance characteristics of CVC3. CVC3 has many useful features, but some +core aspects of the design led to high memory use, and the use of heavyweight +computation (where more nimble engineering approaches could suffice) makes CVC3 +a much slower prover than other tools. As these designs are central to CVC3, a +new version was preferable to a selective re-engineering, which would have +ballooned in short order. -- cgit v1.2.3 From af1714ddc446fe6e239852374f5f628302980488 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 22 Jan 2019 14:43:17 -0600 Subject: Fix parsing of overloaded parametric datatype selectors (#2819) --- src/expr/symbol_table.cpp | 27 ++++++++++++++++++++-- test/regress/CMakeLists.txt | 1 + .../datatypes/repeated-selectors-2769.smt2 | 10 ++++++++ 3 files changed, 36 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/datatypes/repeated-selectors-2769.smt2 diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 32126cf4e..9401e772c 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -203,8 +203,31 @@ Expr OverloadedTypeTrie::getOverloadedFunctionForTypes( if (itc != tat->d_children.end()) { tat = &itc->second; } else { - // no functions match - return d_nullExpr; + Trace("parser-overloading") + << "Could not find overloaded function " << name << std::endl; + // it may be a parametric datatype + TypeNode tna = TypeNode::fromType(argTypes[i]); + if (tna.isParametricDatatype()) + { + Trace("parser-overloading") + << "Parametric overloaded datatype selector " << name << " " + << tna << std::endl; + DatatypeType tnd = static_cast(argTypes[i]); + const Datatype& dt = tnd.getDatatype(); + // tng is the "generalized" version of the instantiated parametric + // type tna + Type tng = dt.getDatatypeType(); + itc = tat->d_children.find(tng); + if (itc != tat->d_children.end()) + { + tat = &itc->second; + } + } + if (tat == nullptr) + { + // no functions match + return d_nullExpr; + } } } // we ensure that there is *only* one active symbol at this node diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c8b052265..77f68aa45 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -371,6 +371,7 @@ set(regress_0_tests regress0/datatypes/rec1.cvc regress0/datatypes/rec2.cvc regress0/datatypes/rec4.cvc + regress0/datatypes/repeated-selectors-2769.smt2 regress0/datatypes/rewriter.cvc regress0/datatypes/sc-cdt1.smt2 regress0/datatypes/some-boolean-tests.cvc diff --git a/test/regress/regress0/datatypes/repeated-selectors-2769.smt2 b/test/regress/regress0/datatypes/repeated-selectors-2769.smt2 new file mode 100644 index 000000000..827b17e36 --- /dev/null +++ b/test/regress/regress0/datatypes/repeated-selectors-2769.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL) +(set-info :status sat) +(declare-datatypes ((t1 1)) ((par (T1) ((mkt1 (p1 T1)))))) +(declare-datatypes ((t2 1)) ((par (T1) ((mkt2 (p1 T1)))))) +(define-fun s1 () (t1 Int) (mkt1 3)) +(define-fun s2 () (t2 Int) (mkt2 3)) +(define-fun s3 () Int (p1 s1)) +(define-fun s4 () Int (p1 s2)) +(assert (= s3 s4)) +(check-sat) -- cgit v1.2.3 From e5f4e2c0c1dc79f9940ddb4fcdbf04d6cffe98f5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 22 Jan 2019 15:48:48 -0600 Subject: Fix tuple and record CVC printing (#2818) --- src/printer/cvc/cvc_printer.cpp | 26 ++++++++++++++++++---- test/regress/CMakeLists.txt | 2 ++ test/regress/regress0/datatypes/tree-get-value.cvc | 10 +++++++++ .../regress0/printer/tuples_and_records.cvc | 18 +++++++++++++++ 4 files changed, 52 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress0/datatypes/tree-get-value.cvc create mode 100644 test/regress/regress0/printer/tuples_and_records.cvc diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index e6ff02f10..36d2ddfb7 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -407,12 +407,30 @@ void CvcPrinter::toStream( case kind::APPLY_SELECTOR_TOTAL: { TypeNode t = n[0].getType(); Node opn = n.getOperator(); - if( t.isTuple() ){ + if (t.isTuple() || t.isRecord()) + { toStream(out, n[0], depth, types, true); + out << '.'; const Datatype& dt = ((DatatypeType)t.toType()).getDatatype(); - int sindex = dt[0].getSelectorIndexInternal( opn.toExpr() ); - Assert( sindex>=0 ); - out << '.' << sindex; + if (t.isTuple()) + { + int sindex; + if (n.getKind() == kind::APPLY_SELECTOR) + { + sindex = Datatype::indexOf(opn.toExpr()); + } + else + { + sindex = dt[0].getSelectorIndexInternal(opn.toExpr()); + } + Assert(sindex >= 0); + out << sindex; + } + else + { + toStream(out, opn, depth, types, false); + } + return; }else{ toStream(op, opn, depth, types, false); } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 77f68aa45..6f147db3c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -377,6 +377,7 @@ set(regress_0_tests regress0/datatypes/some-boolean-tests.cvc regress0/datatypes/stream-singleton.smt2 regress0/datatypes/tenum-bug.smt2 + regress0/datatypes/tree-get-value.cvc regress0/datatypes/tuple-model.cvc regress0/datatypes/tuple-no-clash.cvc regress0/datatypes/tuple-record-bug.cvc @@ -573,6 +574,7 @@ set(regress_0_tests regress0/print_lambda.cvc regress0/printer/bv_consts_bin.smt2 regress0/printer/bv_consts_dec.smt2 + regress0/printer/tuples_and_records.cvc regress0/push-pop/boolean/fuzz_12.smt2 regress0/push-pop/boolean/fuzz_13.smt2 regress0/push-pop/boolean/fuzz_14.smt2 diff --git a/test/regress/regress0/datatypes/tree-get-value.cvc b/test/regress/regress0/datatypes/tree-get-value.cvc new file mode 100644 index 000000000..0a7da7f69 --- /dev/null +++ b/test/regress/regress0/datatypes/tree-get-value.cvc @@ -0,0 +1,10 @@ +% EXPECT: sat +% EXPECT: ((left(x), leaf)) +OPTION "produce-models"; +DATATYPE + tree = node(left : tree, right : tree) | leaf +END; +x : tree; +ASSERT is_leaf(left(x)); +CHECKSAT; +GET_VALUE left(x); diff --git a/test/regress/regress0/printer/tuples_and_records.cvc b/test/regress/regress0/printer/tuples_and_records.cvc new file mode 100644 index 000000000..267a316e8 --- /dev/null +++ b/test/regress/regress0/printer/tuples_and_records.cvc @@ -0,0 +1,18 @@ +% EXPECT: invalid +% EXPECT: ((r.a, "active")) +% EXPECT: ((y.1, 9)) +OPTION "produce-models"; + +R : TYPE = [# + a : STRING, + b : STRING +#]; +r : R; + +y: [REAL, INT, REAL]; + +ASSERT r = (# a := "active", b := "who knows?" #); +ASSERT y = ( 4/5, 9, 11/9 ); +QUERY r.a = "what?"; +GET_VALUE r.a; +GET_VALUE y.1; -- cgit v1.2.3