Permalink
Browse files

[VRG]

- better proving results for vrg-run.pl. (added Hint and
  Pending according to the results of goal-match.xclp)
- updated the test suite to reflect these changes.

git-svn-id: http://svn.berlios.de/svnroot/repos/unisimu/VRG@857 625e195c-0704-0410-94f2-f261ee9f2fe7
  • Loading branch information...
1 parent ae09593 commit 9674a7e4291eb4f025237ecc238cbac5b0d43c87 agent committed Nov 12, 2006
View
@@ -25,6 +25,7 @@ conjunction : clause ',' <commit> conjunction
{ "(and $item{clause} $item{conjunction})" }
+ | '(' <commit> disjunction ')' { $item{disjunction} }
| clause
| <error?> <reject>
@@ -148,8 +149,8 @@ infix_circum_open : { ::match_infix_circum_open($text) }
arguments : <leftop: clause ',' clause> <commit> { join ' ', @{ $item[1] } }
-variable : /\?[A-Za-z_]([-\w])*/ <commit> { $item[1] . $item{identifier} }
- | '?'
+variable : /\$?\?[A-Za-z_]([-\w])*/ <commit> { $item[1] . $item{identifier} }
+ | /\$?\?/
literal : identifier
| number
@@ -26,16 +26,15 @@ module AntiVectorize.
\?l, #?alpha, #?beta, ?l [on] ?alpha, ?alpha [//] ?beta => ?l [~on] ?beta.
\?l, #?alpha, ?l [~T] ?alpha, ?l [~X] ?alpha, ?l [~on] ?alpha => ?l [//] ?alpha.
+\?l, #?alpha, (?l [//] ?alpha; ?l [T] ?alpha; ?l [X] ?alpha) => ?l [~on] ?alpha.
+
/* plane-plane relationships */
#?alpha, #?beta,
~temp(?alpha), ~temp(?beta),
?alpha <?R> ?beta => ?alpha [?R] ?beta.
/* assertions */
-\?l, #?alpha, ?l [on] ?alpha, ?l [~on] ?alpha => contradiction(?l, ?alpha).
-\?l, #?alpha, ?l [on] ?alpha, ?l [//] ?alpha => contradiction(?l, ?alpha).
-\?l, #?alpha, ?l [on] ?alpha, ?l [T] ?alpha => contradiction(?l, ?alpha).
-\?l, #?alpha, ?l [on] ?alpha, ?l [X] ?alpha => contradiction(?l, ?alpha).
+\?l, #?alpha, ?l [on] ?alpha, ?l [~on] ?alpha => contradiction("[on]", "[~on]", ?l, ?alpha).
-contradiction(?, ?) => halt().
+contradiction($?) => halt().
View
@@ -20,8 +20,8 @@ include "vrg-sugar.xclp".
?a <?R> ?b => ?b <?R> ?a.
/* assertions */
-?a <//> ?b, ?a <~//> ?b => contradiction(?a, ?b).
-?a <T> ?b, ?a <~T> ?b => contradiction(?a, ?b).
-?a <T> ?b, ?a <X> ?b => contradiction(?a, ?b).
-?a <X> ?b, ?a <~X> ?b => contradiction(?a, ?b).
-contradiction(?, ?) => halt().
+?a <//> ?b, ?a <~//> ?b => contradiction("<//>", "<~//>", ?a, ?b).
+?a <T> ?b, ?a <~T> ?b => contradiction("<T>", "<~T>", ?a, ?b).
+?a <T> ?b, ?a <X> ?b => contradiction("<T>", "<X>", ?a, ?b).
+?a <X> ?b, ?a <~X> ?b => contradiction("<X>", "<~X>", ?a, ?b).
+contradiction($?) => halt().
View
@@ -34,4 +34,4 @@ module Vectorize.
#?alpha, #?beta, ?alpha [?R] ?beta => ?alpha <?R> ?beta.
/* control rules */
-contradiction(?, ?) => halt().
+contradiction($?) => halt().
View
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
View
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
View
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
View
@@ -37,25 +37,28 @@
}
closedir $dh;
+my $hit;
my @stats;
while (my ($rule_name, $count) = each %rules) {
- my $ratio = sprintf("%.02f%%", "$count.0"/$total_fires*100);
- push @stats, [$rule_name, $count, $ratio];
+ push @stats, [$rule_name, $count];
+ $hit++ if $count > 0;
}
@stats = sort {
my $res = $a->[1] <=> $b->[1];
($res == 0) ? ($a->[0] cmp $b->[0]) : $res;
} @stats;
my $tb = Text::Table->new(
- "Rule", "Count", "Ratio"
+ "Rule", "Count"
);
$tb->load(@stats);
print $tb->rule( '-' );
print $tb->title;
print $tb->rule( '-' );
print $tb->body;
+printf("\nFor total %.02f%% of the rules have been fired.\n",
+ "$hit.0"/scalar(keys %rules)*100);
sub parse_rule_list {
my $log = shift;
View
@@ -11,10 +11,11 @@
use Getopt::Std;
my %opts;
-getopts('tv', \%opts) or help();
+getopts('tvf', \%opts) or help();
$Clips::Batch::Verbose = $opts{v};
my $cover_test = $ENV{VRG_COVER};
+my $no_trim = $opts{f};
my %infix = (
'parallel' => '//',
@@ -86,44 +87,60 @@
$clips->facts(\my $anti_vec_facts);
$clips->focus('GoalMatch');
-$clips->run;
+$clips->run(\my $match_run_log);
$clips->facts('GoalMatch', \my $goal_match_facts);
$clips->eof;
#warn "FACTS: ", $facts;
#warn "GOAL!!! $goal_res\n";
-my @goal;
+my (@solved, @pending, @hint);
#warn $goal_match_facts;
-if ($goal_match_facts =~ /\(contradiction (\S+) (\S+)\)/) {
- print "Contradiction detected. (Check the relationships between $1 and $2.)\n";
+if ($goal_match_facts =~ /\(contradiction (.+)\)/) {
+ my $info = $1;
+ my @item = split ' ', $info;
+ map { s/\"//g } @item;
+ print "Contradiction detected: ",
+ "$item[2] $item[0] $item[3], $item[2] $item[1] $item[3].\n\n";
} else {
- while ($anti_vec_facts =~ /\(goal ([^\)]+)\)/g) {
- push @goal, "($1)";
+ open my $in, '<', \$goal_match_facts or die;
+ while (<$in>) {
+ if (/\(solved (.+)\)$/g) {
+ push @solved, "($1)";
+ #warn "adding solved ($1)";
+ }
+ elsif (/\(pending (.+)\)$/g) {
+ push @pending, "($1)";
+ #warn "adding pending ($1)";
+ }
+ elsif (/\(hint (.+)\)$/g) {
+ push @hint, "($1)";
+ #warn "adding hint ($1)";
+ }
}
- if (@goal == 0) {
- warn "no goal found.\n";
- } else {
- my @missed;
- for my $goal (@goal) {
- my $pat = quotemeta($goal);
- if ($anti_vec_facts !~ /\s+$pat\s*\n/s) {
- push @missed, $goal;
- }
+ close $in;
+
+ my @fmt_pending = map { format_fact($_) } @pending;
+ my @fmt_hint = map { format_fact($_) } @hint;
+ if (@pending == 0) {
+ if (@solved == 0) {
+ print "No goal found.\n\n";
+ } else {
+ print "Yes.\n\n";
}
- if (@missed) {
- if (@goal == 1) {
- print "No.\n";
- } else {
- print "No. (pending: ",
- (join ', ', map { format_fact($_) } @missed), ")\n";
- }
+ } else {
+ if (@solved + @pending == 1) {
+ print "No.\n";
} else {
- print "Yes.\n";
+ print "No.\nPending: ", join(', ', @fmt_pending), "\n";
+ }
+ if (@hint) {
+ print "Hint: ", join(', ', @fmt_hint), "\n";
}
+ print "\n";
}
}
@@ -151,7 +168,7 @@
$painter->draw(
outfile => $fname,
fact_filter => \&format_fact,
- trim => 1,
+ trim => $no_trim ? 0 : 1,
);
warn "generating $fname...\n";
@@ -160,7 +177,7 @@
$painter->draw(
outfile => $fname,
fact_filter => \&format_fact,
- trim => 1,
+ trim => $no_trim ? 0 : 1,
);
warn "generating $fname...\n";
@@ -169,7 +186,7 @@
$painter->draw(
outfile => $fname,
fact_filter => \&format_fact,
- trim => 1,
+ trim => $no_trim ? 0 : 1,
);
warn "generating $fname...\n";
@@ -181,8 +198,8 @@
$painter->draw(
outfile => $fname,
fact_filter => \&format_fact,
- trim => 1,
- goals => \@goal,
+ trim => $no_trim ? 0 : 1,
+ goals => (@pending == 0 ? \@solved : undef),
);
warn "generating $fname...\n";
@@ -206,7 +223,7 @@
$fname = "$db_dir/$base-$rand.yml";
last if !-e $fname;
}
- YAML::Syck::DumpFile($fname, [$rule_list, $run_log]);
+ YAML::Syck::DumpFile($fname, [$rule_list, $run_log . $match_run_log]);
}
sub help {
View
@@ -62,8 +62,8 @@ sub run_test () {
warn $stderr if $stderr;
#warn $stdout;
- $stdout =~ s/^[^\n]*\n//i;
- my $ans_got = $&;
+ $stdout =~ s/^(.*?\n)\n//s;
+ my $ans_got = $1;
my ($vectorize, $eval, $final) = ($stdout =~ /(.*)---\n(.*)---\n(.*)/s);
if (defined $block->vectorize) {
View
@@ -15,3 +15,4 @@ a on alpha, b on alpha, meet(a, b, P) => a // alpha
--- ans
No.
+Hint: a [~X] alpha, a [~T] alpha, a [on] alpha
View
@@ -14,7 +14,7 @@ line a, b;
a T b, a//b => a//b
--- ans
-Contradiction detected. (Check the relationships between a and b.)
+Contradiction detected: a <//> b, a <~//> b.
@@ -26,7 +26,7 @@ line a, b, c, d;
a T b, b // c, c // a => a // c
--- ans
-Contradiction detected. (Check the relationships between b and c.)
+Contradiction detected: b <//> c, b <~//> c.
@@ -40,7 +40,7 @@ line l; plane alpha;
l on alpha, l // alpha => l // alpha
--- ans
-Contradiction detected. (Check the relationships between l and alpha.)
+Contradiction detected: l [on] alpha, l [~on] alpha.
@@ -52,7 +52,7 @@ plane a, b;
a T b, a // b => a T b
--- ans
-Contradiction detected. (Check the relationships between a and b.)
+Contradiction detected: a <//> b, a <~//> b.
@@ -65,4 +65,4 @@ plane alpha;
l // alpha, l X alpha => l // alpha
--- ans
-Contradiction detected. (Check the relationships between l and alpha.)
+Contradiction detected: l <T> alpha, l <X> alpha.
View
@@ -91,6 +91,7 @@ a [~X] alpha
--- ans
No.
+Hint: a [~X] alpha, a [~T] alpha
@@ -119,6 +120,7 @@ a [~X] alpha
--- ans
No.
+Hint: a [~X] alpha, a [~T] alpha
@@ -145,6 +147,7 @@ a [~T] alpha
--- ans
No.
+Hint: a [~X] alpha, a [~T] alpha
@@ -348,7 +351,8 @@ line m, n;
alpha T beta, n on alpha, m on beta, m T n => n T beta, m T alpha;
--- ans
-No. (pending: n [T] beta, m [T] alpha)
+No.
+Pending: m [T] alpha, n [T] beta
@@ -364,7 +368,8 @@ line m, n;
alpha T beta, n on alpha, m on beta, m T n => n ~T beta, m ~T alpha;
--- ans
-No. (pending: n [~T] beta, m [~T] alpha)
+No.
+Pending: m [~T] alpha, n [~T] beta
@@ -391,8 +396,9 @@ line m, n;
alpha T beta, n on alpha, m on beta, m T n => beta T alpha, m // n
--- ans
-No. (pending: m [//] n)
-
+No.
+Pending: m [//] n
+Hint: m [~//] n, m [T] n
=== TEST 19: (常规方法中,处理面面垂直问题多半是要作出交线的垂线的。)

0 comments on commit 9674a7e

Please sign in to comment.