added real estate python3 and added change name functions to conjectu…

c/expressions.c

@@ -15,7 +15,9 @@
 #include <signal.h>
 #include <unistd.h>
 #include <float.h>
-#include <malloc.h>
+#include <time.h>
+#include <limits.h>
+//#include <malloc.h>
 
 #include "bintrees.h"
 #include "util.h"
@@ -121,7 +123,7 @@ unsigned long int treeCount = 0;
 unsigned long int labeledTreeCount = 0;
 unsigned long int validExpressionsCount = 0;
 
-int maximum_complexity_reached = -1;
+unsigned long int complexity = 0;
 boolean report_maximum_complexity_reached = FALSE;
 
 unsigned long int timeOut = 0;
@@ -131,6 +133,8 @@ boolean userInterrupted = FALSE;
 boolean terminationSignalReceived = FALSE;
 
 boolean heuristicStoppedGeneration = FALSE;
+unsigned long int complexity_limit = (INT_MAX) ;
+boolean complexity_limit_reached = FALSE;
 
 boolean onlyUnlabeled = FALSE;
 boolean onlyLabeled = FALSE;
@@ -210,9 +214,12 @@ inline void dalmatianUpdateHitCount(){
 
 }
 
-void dalmatianHeuristic(TREE *tree, double *values){
+void dalmatianHeuristic(TREE *tree, double *values, int skipCount){
     int i;
     //this heuristic assumes the expression was true for all objects
+    if(skipCount > allowedPercentageOfSkips * objectCount){
+      return;
+    }
 
     //if known theory is provided, we check that first
     boolean isMoreSignificant = FALSE;
@@ -247,6 +254,7 @@ void dalmatianHeuristic(TREE *tree, double *values){
         dalmatianFirst = FALSE;
         dalmatianUpdateHitCount();
         return;
+
     }
 
     //check the significance
@@ -259,9 +267,9 @@ void dalmatianHeuristic(TREE *tree, double *values){
     for(i=0; i<objectCount; i++){
         double currentBest = 
         dalmatianCurrentConjectureValues[dalmatianBestConjectureForObject[i]][i];
-        if(handleComparator(currentBest, values[i], inequality)){
+        if(handleComparator(currentBest, values[i], inequality+1)){
             conjectureFrequency[dalmatianBestConjectureForObject[i]]++;
-        } else {
+        } else if (handleComparator(values[i], currentBest, inequality+1) ) {
             if(verbose){
                 fprintf(stderr, "Conjecture is more significant for object %d.\n", i+1);
                 fprintf(stderr, "%11.6lf vs. %11.6lf\n", currentBest, values[i]);
@@ -284,7 +292,7 @@ void dalmatianHeuristic(TREE *tree, double *values){
     int smallestAvailablePosition = 0;
 
     while(smallestAvailablePosition < objectCount &&
-            conjectureFrequency[smallestAvailablePosition]>0){
+            conjectureFrequency[smallestAvailablePosition]>0){  // checking whether an expression is dropped
         smallestAvailablePosition++;
     }
     if(smallestAvailablePosition == objectCount){
@@ -423,9 +431,12 @@ inline void dalmatianUpdateHitCount_propertyBased(){
 
 }
 
-void dalmatianHeuristic_propertyBased(TREE *tree, boolean *values){
+void dalmatianHeuristic_propertyBased(TREE *tree, boolean *values, int skipCount){
     int i;
     //this heuristic assumes the expression was true for all objects
+    if(skipCount > allowedPercentageOfSkips * objectCount){
+      return;
+    }
 
     //if known theory is provided, we check that first
     boolean isMoreSignificant = FALSE;
@@ -731,7 +742,7 @@ void grinvinHeuristicPostProcessing(){
 
 //------ Stop generation -------
 
-boolean shouldGenerationProcessBeTerminated(){
+boolean shouldGenerationProcessBeTerminated(int complexity){
     if(heuristicStopConditionReached!=NULL){
         if(heuristicStopConditionReached()){
             heuristicStoppedGeneration = TRUE;
@@ -741,6 +752,11 @@ boolean shouldGenerationProcessBeTerminated(){
     if(timeOutReached || userInterrupted || terminationSignalReceived){
         return TRUE;
     }
+    if (complexity > complexity_limit) {
+        complexity_limit_reached = TRUE;
+        complexity = complexity_limit;
+        return TRUE;
+    }
 
     return FALSE;
 }
@@ -869,7 +885,7 @@ void handleExpression(TREE *tree, double *values, int calculatedValues, int hitC
             if(skipCount > allowedPercentageOfSkips * objectCount){
                 return;
             }
-            dalmatianHeuristic(tree, values);
+            dalmatianHeuristic(tree, values, skipCount);
         } else if(selectedHeuristic==GRINVIN_HEURISTIC){
             if(skipCount > allowedPercentageOfSkips * objectCount){
                 return;
@@ -889,7 +905,7 @@ void handleExpression_propertyBased(TREE *tree, boolean *values, int calculatedV
             if(skipCount > allowedPercentageOfSkips * objectCount){
                 return;
             }
-            dalmatianHeuristic_propertyBased(tree, values);
+            dalmatianHeuristic_propertyBased(tree, values, skipCount);
         } else if(selectedHeuristic==GRINVIN_HEURISTIC){
             BAILOUT("Grinvin heuristic is not defined for property-based conjectures.")
         }
@@ -1026,6 +1042,9 @@ void writeNonCommutativeBinaryOperatorExample(FILE *f){
 }
 
 boolean handleComparator(double left, double right, int id){
+    if ((isnan(left)) || isnan(right)) {
+      return TRUE;
+    }
     if(id==0){
         return left <= right;
     } else if(id==1){
@@ -1282,7 +1301,8 @@ void generateLabeledTree(TREE *tree, NODE **orderedNodes, int pos){
                     generateLabeledTree(tree, orderedNodes, pos+1);
                     invariantsUsed[i] = FALSE;
                 }
-                if(shouldGenerationProcessBeTerminated()){
+                complexity = targetUnary + 2*targetBinary;
+                if(shouldGenerationProcessBeTerminated(complexity)){
                     return;
                 }
             }
@@ -1291,7 +1311,8 @@ void generateLabeledTree(TREE *tree, NODE **orderedNodes, int pos){
             for (i=0; i<unaryOperatorCount; i++){
                 currentNode->contentLabel[1] = unaryOperators[i];
                 generateLabeledTree(tree, orderedNodes, pos+1);
-                if(shouldGenerationProcessBeTerminated()){
+                complexity = targetUnary + 2*targetBinary;
+                if(shouldGenerationProcessBeTerminated(complexity)){
                     return;
                 }
             }
@@ -1301,7 +1322,8 @@ void generateLabeledTree(TREE *tree, NODE **orderedNodes, int pos){
             for (i=0; i<nonCommBinaryOperatorCount; i++){
                 currentNode->contentLabel[1] = nonCommBinaryOperators[i];
                 generateLabeledTree(tree, orderedNodes, pos+1);
-                if(shouldGenerationProcessBeTerminated()){
+                complexity = targetUnary + 2*targetBinary;
+                if(shouldGenerationProcessBeTerminated(complexity)){
                     return;
                 }
             }
@@ -1312,7 +1334,8 @@ void generateLabeledTree(TREE *tree, NODE **orderedNodes, int pos){
                 for (i=0; i<commBinaryOperatorCount; i++){
                     currentNode->contentLabel[1] = commBinaryOperators[i];
                     generateLabeledTree(tree, orderedNodes, pos+1);
-                    if(shouldGenerationProcessBeTerminated()){
+                    complexity = targetUnary + 2*targetBinary;
+                    if(shouldGenerationProcessBeTerminated(complexity)){
                         return;
                     }
                 }
@@ -1370,7 +1393,8 @@ void generateTreeImpl(TREE *tree){
         addChildToNodeInTree(tree, parent);
         generateTreeImpl(tree);
         removeChildFromNodeInTree(tree, parent);
-        if(shouldGenerationProcessBeTerminated()){
+        complexity = targetUnary + 2*targetBinary;
+        if(shouldGenerationProcessBeTerminated(complexity)){
             return;
         }
     }
@@ -1380,7 +1404,8 @@ void generateTreeImpl(TREE *tree){
         addChildToNodeInTree(tree, parent);
         generateTreeImpl(tree);
         removeChildFromNodeInTree(tree, parent);
-        if(shouldGenerationProcessBeTerminated()){
+        complexity = targetUnary + 2*targetBinary;
+        if(shouldGenerationProcessBeTerminated(complexity)){
             return;
         }
     }
@@ -1391,9 +1416,7 @@ void generateTree(int unary, int binary){
         fprintf(stderr, "Generating trees with %d unary node%s and %d binary node%s.\n",
                 unary, unary == 1 ? "" : "s", binary, binary == 1 ? "" : "s");
     }
-    if(report_maximum_complexity_reached){//no need to check if this is larger since we generate them in increasing order
-        maximum_complexity_reached = 2*binary + unary;
-    }
+
     TREE tree;
     targetUnary = unary;
     targetBinary = binary;
@@ -1445,7 +1468,8 @@ void conjecture(int startUnary, int startBinary){
 
     generateTree(unary, binary);
     getNextOperatorCount(&unary, &binary);
-    while(!shouldGenerationProcessBeTerminated()) {
+    complexity = unary + 2*binary;
+    while(!shouldGenerationProcessBeTerminated(complexity)) {
         if(unary <= MAX_UNARY_COUNT && 
            binary <= MAX_BINARY_COUNT &&
            availableInvariants >= binary+1)
@@ -2079,15 +2103,16 @@ int processOptions(int argc, char **argv) {
         {"operators", required_argument, NULL, 0},
         {"invariants", required_argument, NULL, 0},
         {"leq", no_argument, NULL, 0},
-        {"less", no_argument, NULL, 0},
+        {"less", no_argument, NULL, 0}, // don't use this option
         {"geq", no_argument, NULL, 0},
-        {"greater", no_argument, NULL, 0},
+        {"greater", no_argument, NULL, 0}, // don't use this option
         {"limits", required_argument, NULL, 0},
         {"allowed-skips", required_argument, NULL, 0},
         {"print-valid-expressions", no_argument, NULL, 0},
         {"sufficient", no_argument, NULL, 0},
         {"necessary", no_argument, NULL, 0},
         {"maximum-complexity", no_argument, NULL, 0},
+        {"complexity-limit", required_argument, NULL, 0},
         {"help", no_argument, NULL, 'h'},
         {"verbose", no_argument, NULL, 'v'},
         {"unlabeled", no_argument, NULL, 'u'},
@@ -2191,6 +2216,9 @@ int processOptions(int argc, char **argv) {
                     case 21:
                         report_maximum_complexity_reached = TRUE;
                         break;
+                    case 22:
+                        complexity_limit = strtoul(optarg, NULL, 10);
+                        break;
                     default:
                         fprintf(stderr, "Illegal option index %d.\n", option_index);
                         usage(name);
@@ -2310,6 +2338,10 @@ int processOptions(int argc, char **argv) {
 
 int main(int argc, char *argv[]) {
 
+    time_t start, end;
+
+    start = time(NULL);
+
     operatorFile = stdin;
     invariantsFile = stdin;
 
@@ -2418,6 +2450,8 @@ int main(int argc, char *argv[]) {
         fprintf(stderr, "Generation process was interrupted by user.\n");
     } else if(terminationSignalReceived){
         fprintf(stderr, "Generation process was killed.\n");
+    } else if(complexity_limit_reached){
+        fprintf(stderr, "Generation process was stopped because the maximum complexity was explored.\n");
     }
 
     //print some statistics
@@ -2434,15 +2468,14 @@ int main(int argc, char *argv[]) {
         fprintf(stderr, "Found %lu labeled trees.\n", labeledTreeCount);
         fprintf(stderr, "Found %lu valid expressions.\n", validExpressionsCount);
     }
-
-    if(report_maximum_complexity_reached){
-        fprintf(stderr, "Maximum complexity reached was %d\n", maximum_complexity_reached);
-    }
+    fprintf(stderr, "Maximum complexity reached: %lu\n", complexity-1);
 
     //do some heuristic-specific post-processing like outputting the conjectures
     if(heuristicPostProcessing!=NULL){
         heuristicPostProcessing();
     }
+    end = time(NULL);
+    fprintf(stderr, "Elapsed time: %ld seconds\n", end - start);
 
     return 0;
 }