CVC4's native language - Revision history

Taking: /* Commands */

2016-01-08T06:07:46Z

‎Commands

Taking: /* RESTART */

2016-01-08T06:07:19Z

‎RESTART

Taking: /* PUSH and POP */

2016-01-06T08:05:15Z

‎PUSH and POP

Taking: /* Commands */

2016-01-06T08:02:04Z

‎Commands

Tinelli: /* Global symbol definitions */

2015-11-01T18:06:09Z

‎Global symbol definitions

Tinelli: /* Terms and Formulas */

2015-11-01T17:55:13Z

‎Terms and Formulas

Mdeters: /* Tuples and Records */

2013-09-17T00:04:15Z

‎Tuples and Records

Mdeters: /* Tuples and Records */

2013-09-16T23:57:07Z

‎Tuples and Records

Mdeters: /* Record Types */

2013-09-16T23:54:57Z

‎Record Types

Mdeters: /* Tuple Types */

2013-09-16T23:54:33Z

‎Tuple Types

@@ Line 985: / Line 985: @@
 * <math>\mathrm{PUSHTO}</math>
 * <math>\mathrm{POPTO}</math>
 Here, we explain some of the above commands in more detail.

@@ Line 1,031: / Line 1,031: @@
 The command <math>\mathrm{CHECKSAT}\ F</math> behaves identically
 to <math>\mathrm{QUERY}\ \mathrm{NOT}\ F</math>.
 === COUNTERMODEL ===

@@ Line 1,074: / Line 1,074: @@
 is added to the most recent assertion level.
 Executing POP n removes from the context the most recent n assertion levels and all the formulas in them.
 Note that formulas at assertion level 0 cannot be retracted.

@@ Line 959: / Line 959: @@
 * <math>\mathrm{ASSERT}\ F</math> -- Add the formula <math>F</math> to the current logical context <math>\Gamma</math>.
 * [[#CHECKSAT|<math>\mathrm{CHECKSAT}\ F</math>]] -- Check if the formula <math>F</math> is satisfiable in the current logical context (<math>\Gamma \not\models_T \mathrm{NOT}\ F</math>).
 * [[#COUNTEREXAMPLE|<math>\mathrm{COUNTEREXAMPLE}</math>]] -- After an invalid <math>\mathrm{QUERY}</math> or satisfiable <math>\mathrm{CHECKSAT}</math>, print the context that is a witness for invalidity/satisfiability.
 * [[#COUNTERMODEL|<math>\mathrm{COUNTERMODEL}</math>]] -- After an invalid <math>\mathrm{QUERY}</math> or satisfiable <math>\mathrm{CHECKSAT}</math>, print a model that makes the formula invalid/satisfiable. The model is provided in terms of concrete values for each free symbol.
 * <math>\mathrm{OPTION}\ o\ v</math> -- Set the command-line option flag <math>o</math> to value <math>v</math>. The argument <math>o</math> is provide as a string literal enclosed in double-quotes and <math>v</math> as an integer value.
-* <math>\mathrm{POP}</math> -- Equivalent to <math>\mathrm{POPTO}\ 1</math>
+* [[#PUSH and POP|<math>\mathrm{POP}</math>]] -- Restore the system to the state it was in right before the most recent call to <math>\mathrm{PUSH}</math>.
-* [[#PUSH and POPTO|<math>\mathrm{POPTO}\ n</math>]] -- Restore the system to the state it was in right before the most recent call to <math>\mathrm{PUSH}</math> made from assertion (stack) level <math>n</math>. Note that the current assertion level is printed as part of the output of the <math>\mathrm{WHERE}</math> command.
+* [[#PUSH and POP|<math>\mathrm{POP}\ n</math>]] -- Equivalent to <math>\mathrm{POP}</math> repeated <math>n</math> times.
-* [[#PUSH and POPTO|<math>\mathrm{PUSH}</math>]] -- Save (checkpoint) the current state of the system.
+* [[#PUSH and POP|<math>\mathrm{PUSH}</math>]] -- Save (checkpoint) the current state of the system.
 * [[#QUERY|<math>\mathrm{QUERY}\ F</math>]] -- Check if the formula <math>F</math> is valid in the current logical context (<math>\Gamma\models_T F</math>).
 * [[#RESTART|<math>\mathrm{RESTART}\ F</math>]] -- After an invalid <math>\mathrm{QUERY}</math> or satisfiable <math>\mathrm{CHECKSAT}</math>, repeat the check but with the additional assumption <math>F</math> in the context.
@@ Line 979: / Line 979: @@
 * <math>\mathrm{UNTRACE}\ f</math> -- Turn off tracing for the debug flag <math>f</math>.
 Here, we explain some of the above commands in more detail.
@@ Line 1,059: / Line 1,065: @@
 [More]
-=== PUSH and POPTO ===
+=== PUSH and POP ===
@@ Line 1,067: / Line 1,073: @@
 Each formula added to the context either by the user, via an ASSERT command, or internally by the system
 is added to the most recent assertion level.
-Executing POPTO n removes from the context the most recent n assertion levels and all the formulas in them.
+Executing POP n removes from the context the most recent n assertion levels and all the formulas in them.
 So, for instance, POP 1 has the effect of retracting all formulas in the current assertion level (and removing that level).
 Note that formulas at assertion level 0 cannot be retracted.
-Note: Symbol declarations are always added at assertion level zero. So they are not affected by POPTO commands.
+Note: Symbol declarations are always added at assertion level zero. So they are not affected by POP commands.
 == Instantiation Patterns ==

@@ Line 553: / Line 553: @@
 It is much more efficient to associate a complex term with a name directly rather than
 to declare a constant and later assert that it is equal to the same term.
-This point is explained in more detail later in section [[Commands | Commands]].
+This point is explained in more detail later in section [[#Commands | Commands]].
 More generally, in CVC4 one can associate a term to function symbols of any arity.

@@ Line 517: / Line 517: @@
   % Propositional "variables"
-  P, Q; BOOLEAN;
+  P, Q: BOOLEAN;
 Like type declarations, function symbol declarations like the above have global scope

@@ Line 871: / Line 871: @@
 Externally, tuples and records have their own syntax for constructor and selector operators.
 * Records of type <math>[\#\ l_0:T_0, \ldots, l_n:T_n\ \#]</math> have the associated  record constructor <math>(\#\ l_0 := \_,\; \ldots,\; l_n := \_\ \#)</math> whose arguments must be terms of type <math>T_0, \ldots, T_n</math>, respectively.
-* Tuples of type <math>[\ T_0, \ldots, T_n\ ]</math> have the associated tuple constructor <math>(\ \_,\; \ldots,\; \_\ )</math> whose arguments must be terms of type <math>T_0, \ldots, T_n</math>, respectively.  Note that the empty tuple can be created with <math>()</math>; however, a single-element tuple cannot be directly created, as <math>(\ \_\ )</math> is interpreted as a parenthesized (non-tuple) expression.
+* Tuples of type <math>[\ T_0, \ldots, T_n\ ]</math> have the associated tuple constructor <math>(\ \_,\; \ldots,\; \_\ )</math> whose arguments must be terms of type <math>T_0, \ldots, T_n</math>, respectively.  Note that the empty tuple can be created with <math>(\ )</math>; however, a single-element tuple cannot be directly created, as <math>(\ \_\ )</math> is interpreted as a parenthesized (non-tuple) expression.
 The selector operators on records and tuples follows a dot notation syntax.

@@ Line 179: / Line 179: @@
 </center>
-where <math>n > 0</math>, <math>l_1,\ldots, l_n</math> are field labels,
+where <math>n \geq 0</math>, <math>l_1,\ldots, l_n</math> are field labels,
 and the arguments can be instantiated with any first-order types.

@@ Line 143: / Line 143: @@
 <center>
 <math>
-\begin{array}{l} [\ ] \\[1ex] [\ \_\ ] \\[1ex] [\ \_\ ,\ \_\ ] \\[1ex] [\ \_\ ,\ \_\ \ ,\ \_\ ] \\[1ex] \ldots \end{array}
+\begin{array}{l} [\ \_\ ] \\[1ex] [\ \_\ ,\ \_\ ] \\[1ex] [\ \_\ ,\ \_\ \ ,\ \_\ ] \\[1ex] \ldots \end{array}
 </math>
 </center>